Let X be given.
We will prove normal_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 one_point_sets_closed X (discrete_topology X) ∧ ∀A B : set, closed_in X (discrete_topology X) A → closed_in X (discrete_topology X) B → A ∩ B = Empty → ∃U V : set, U ∈ discrete_topology X ∧ V ∈ discrete_topology X ∧ A ⊆ U ∧ B ⊆ V ∧ U ∩ V = Empty.
Apply andI to the current goal.
We will prove topology_on X (discrete_topology X) ∧ ∀x : set, x ∈ X → closed_in X (discrete_topology X) {x}.
Apply andI to the current goal.
An exact proof term for the current goal is HTx.
Let x be given.
Assume HxX: x ∈ X.
We will prove closed_in X (discrete_topology X) {x}.
Set U to be the term X ∖ {x}.
We prove the intermediate claim HUsub: U ⊆ X.
Apply setminus_Subq to the current goal.
We prove the intermediate claim HUopen: U ∈ discrete_topology X.
An exact proof term for the current goal is (discrete_open_all X U HUsub).
We prove the intermediate claim HclosedComp: closed_in X (discrete_topology X) (X ∖ U).
An exact proof term for the current goal is (closed_of_open_complement X (discrete_topology X) U HTx HUopen).
We prove the intermediate claim HsingSub: {x} ⊆ X.
An exact proof term for the current goal is (singleton_subset x X HxX).
We prove the intermediate claim Heq: X ∖ U = {x}.
We prove the intermediate claim HUdef: U = X ∖ {x}.
Use reflexivity.
rewrite the current goal using HUdef (from left to right).
An exact proof term for the current goal is (setminus_setminus_eq X {x} HsingSub).
rewrite the current goal using Heq (from right to left).
An exact proof term for the current goal is HclosedComp.
Let A and B be given.
Assume HA: closed_in X (discrete_topology X) A.
Assume HB: closed_in X (discrete_topology X) B.
Assume Hdisj: A ∩ B = Empty.
We will prove ∃U V : set, U ∈ discrete_topology X ∧ V ∈ discrete_topology X ∧ A ⊆ U ∧ B ⊆ V ∧ U ∩ V = Empty.
We use A to witness the existential quantifier.
We use B to witness the existential quantifier.
We prove the intermediate claim HAsub: A ⊆ X.
An exact proof term for the current goal is (closed_in_subset X (discrete_topology X) A HA).
We prove the intermediate claim HBsub: B ⊆ X.
An exact proof term for the current goal is (closed_in_subset X (discrete_topology X) B HB).
We prove the intermediate claim HAopen: A ∈ discrete_topology X.
An exact proof term for the current goal is (discrete_open_all X A HAsub).
We prove the intermediate claim HBopen: B ∈ discrete_topology X.
An exact proof term for the current goal is (discrete_open_all X B HBsub).
Apply andI to the current goal.
We will prove ((A ∈ discrete_topology X ∧ B ∈ discrete_topology X) ∧ A ⊆ A) ∧ B ⊆ B.
Apply andI to the current goal.
We will prove (A ∈ discrete_topology X ∧ B ∈ discrete_topology X) ∧ A ⊆ A.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HAopen.
An exact proof term for the current goal is HBopen.
An exact proof term for the current goal is (Subq_ref A).
An exact proof term for the current goal is (Subq_ref B).
An exact proof term for the current goal is Hdisj.
∎