Let X be given.
We will prove Hausdorff_space X (discrete_topology X).
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) ∧ ∀x1 x2 : set, x1 ∈ X → x2 ∈ X → x1 ≠ x2 → ∃U V : set, U ∈ discrete_topology X ∧ V ∈ discrete_topology X ∧ x1 ∈ U ∧ x2 ∈ V ∧ U ∩ V = Empty.
Apply andI to the current goal.
An exact proof term for the current goal is HTx.
Let x1 and x2 be given.
Assume Hx1X: x1 ∈ X.
Assume Hx2X: x2 ∈ X.
Assume Hneq: x1 ≠ x2.
We will prove ∃U V : set, U ∈ discrete_topology X ∧ V ∈ discrete_topology X ∧ x1 ∈ U ∧ x2 ∈ V ∧ U ∩ V = Empty.
We use {x1} to witness the existential quantifier.
We use {x2} to witness the existential quantifier.
We prove the intermediate claim HUopen: {x1} ∈ discrete_topology X.
We prove the intermediate claim Hsx1: {x1} ⊆ X.
An exact proof term for the current goal is (singleton_subset x1 X Hx1X).
An exact proof term for the current goal is (discrete_open_all X {x1} Hsx1).
We prove the intermediate claim HVopen: {x2} ∈ discrete_topology X.
We prove the intermediate claim Hsx2: {x2} ⊆ X.
An exact proof term for the current goal is (singleton_subset x2 X Hx2X).
An exact proof term for the current goal is (discrete_open_all X {x2} Hsx2).
We prove the intermediate claim Hdisj: {x1} ∩ {x2} = Empty.
Apply Empty_Subq_eq to the current goal.
Let z be given.
Assume Hz: z ∈ {x1} ∩ {x2}.
We will prove z ∈ Empty.
We prove the intermediate claim Hz1: z ∈ {x1}.
An exact proof term for the current goal is (binintersectE1 {x1} {x2} z Hz).
We prove the intermediate claim Hz2: z ∈ {x2}.
An exact proof term for the current goal is (binintersectE2 {x1} {x2} z Hz).
We prove the intermediate claim Hzx1: z = x1.
An exact proof term for the current goal is (SingE x1 z Hz1).
We prove the intermediate claim Hzx2: z = x2.
An exact proof term for the current goal is (SingE x2 z Hz2).
We prove the intermediate claim Hx1x2: x1 = x2.
rewrite the current goal using Hzx1 (from right to left).
rewrite the current goal using Hzx2 (from right to left).
Use reflexivity.
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hneq Hx1x2).
Apply and5I to the current goal.
An exact proof term for the current goal is HUopen.
An exact proof term for the current goal is HVopen.
An exact proof term for the current goal is (SingI x1).
An exact proof term for the current goal is (SingI x2).
An exact proof term for the current goal is Hdisj.
∎