Let X, Tx, Y, Ty and x be given.
Assume HTx: topology_on X Tx.
Assume HTy: topology_on Y Ty.
Assume HxY: x ∈ Y.
We will prove continuous_map X Tx Y Ty (const_fun X x).
We will prove topology_on X Tx ∧ topology_on Y Ty ∧ function_on (const_fun X x) X Y ∧ ∀V : set, V ∈ Ty → preimage_of X (const_fun X x) V ∈ Tx.
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HTx.
An exact proof term for the current goal is HTy.
Let a be given.
Assume HaX: a ∈ X.
We will prove apply_fun (const_fun X x) a ∈ Y.
We prove the intermediate claim Happ: apply_fun (const_fun X x) a = x.
An exact proof term for the current goal is (const_fun_apply X x a HaX).
rewrite the current goal using Happ (from left to right).
An exact proof term for the current goal is HxY.
Let V be given.
Assume HV: V ∈ Ty.
We prove the intermediate claim Hcases: x ∈ V ∨ x ∉ V.
An exact proof term for the current goal is (xm (x ∈ V)).
Apply (Hcases (preimage_of X (const_fun X x) V ∈ Tx)) to the current goal.
Assume HxV: x ∈ V.
We prove the intermediate claim Heq: preimage_of X (const_fun X x) V = X.
Apply set_ext to the current goal.
Let a be given.
Assume Ha: a ∈ preimage_of X (const_fun X x) V.
We will prove a ∈ X.
Apply (SepE X (λu ⇒ apply_fun (const_fun X x) u ∈ V) a Ha) to the current goal.
Assume HaX.
Assume _.
An exact proof term for the current goal is HaX.
Let a be given.
Assume HaX: a ∈ X.
We will prove a ∈ preimage_of X (const_fun X x) V.
We will prove a ∈ {u ∈ X|apply_fun (const_fun X x) u ∈ V}.
Apply (SepI X (λu ⇒ apply_fun (const_fun X x) u ∈ V) a HaX) to the current goal.
We prove the intermediate claim Happ: apply_fun (const_fun X x) a = x.
An exact proof term for the current goal is (const_fun_apply X x a HaX).
rewrite the current goal using Happ (from left to right).
An exact proof term for the current goal is HxV.
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is (topology_has_X X Tx HTx).
Assume HxVn: x ∉ V.
We prove the intermediate claim Heq: preimage_of X (const_fun X x) V = Empty.
Apply set_ext to the current goal.
Let a be given.
Assume Ha: a ∈ preimage_of X (const_fun X x) V.
We will prove a ∈ Empty.
Apply FalseE to the current goal.
Apply (SepE X (λu ⇒ apply_fun (const_fun X x) u ∈ V) a Ha) to the current goal.
Assume HaX.
Assume Hav.
We prove the intermediate claim Happ: apply_fun (const_fun X x) a = x.
An exact proof term for the current goal is (const_fun_apply X x a HaX).
We prove the intermediate claim HxV: x ∈ V.
rewrite the current goal using Happ (from right to left).
An exact proof term for the current goal is Hav.
An exact proof term for the current goal is (HxVn HxV).
Let a be given.
Assume HaE: a ∈ Empty.
We will prove a ∈ preimage_of X (const_fun X x) V.
Apply FalseE to the current goal.
An exact proof term for the current goal is (EmptyE a HaE).
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is (topology_has_empty X Tx HTx).
∎