Let X, Y, Ty and f be given.
Assume HTy: topology_on Y Ty.
Assume Hfun: function_on f X Y.
We will prove continuous_map X (discrete_topology X) Y Ty f.
We prove the intermediate claim HTx: topology_on X (discrete_topology X).
An exact proof term for the current goal is (discrete_topology_on X).
We will prove topology_on X (discrete_topology X) ∧ topology_on Y Ty ∧ function_on f X Y ∧ ∀V : set, V ∈ Ty → preimage_of X f V ∈ discrete_topology X.
Apply andI to the current goal.
We will prove (topology_on X (discrete_topology X) ∧ topology_on Y Ty) ∧ function_on f X Y.
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 Hfun.
Let V be given.
Assume HV: V ∈ Ty.
We will prove preimage_of X f V ∈ discrete_topology X.
We prove the intermediate claim Hsub: preimage_of X f V ⊆ X.
Let x be given.
Assume Hx: x ∈ preimage_of X f V.
An exact proof term for the current goal is (SepE1 X (λu ⇒ apply_fun f u ∈ V) x Hx).
An exact proof term for the current goal is (discrete_open_all X (preimage_of X f V) Hsub).
∎