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_total X Tx Y Ty (const_fun X x).
We will prove ((topology_on X Tx ∧ topology_on Y Ty) ∧ total_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.
An exact proof term for the current goal is (const_fun_total_function_on X Y x HxY).
We prove the intermediate claim Hc: continuous_map X Tx Y Ty (const_fun X x).
An exact proof term for the current goal is (const_fun_continuous X Tx Y Ty x HTx HTy HxY).
An exact proof term for the current goal is (andER ((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) Hc).
∎