We will prove regular_space Sorgenfrey_line Sorgenfrey_topology.
We will prove one_point_sets_closed Sorgenfrey_line Sorgenfrey_topology ∧ ∀x : set, x ∈ Sorgenfrey_line → ∀F : set, closed_in Sorgenfrey_line Sorgenfrey_topology F → x ∉ F → ∃U V : set, U ∈ Sorgenfrey_topology ∧ V ∈ Sorgenfrey_topology ∧ x ∈ U ∧ F ⊆ V ∧ U ∩ V = Empty.
Apply andI to the current goal.
We will prove topology_on Sorgenfrey_line Sorgenfrey_topology ∧ ∀x : set, x ∈ Sorgenfrey_line → closed_in Sorgenfrey_line Sorgenfrey_topology {x}.
Apply andI to the current goal.
An exact proof term for the current goal is (Hausdorff_space_topology Sorgenfrey_line Sorgenfrey_topology Sorgenfrey_line_Hausdorff).
Let x be given.
Assume Hx: x ∈ Sorgenfrey_line.
An exact proof term for the current goal is (Hausdorff_singletons_closed Sorgenfrey_line Sorgenfrey_topology x Sorgenfrey_line_Hausdorff Hx).
Let x be given.
Assume HxR: x ∈ Sorgenfrey_line.
Let F be given.
Assume HFcl: closed_in Sorgenfrey_line Sorgenfrey_topology F.
Assume HxnotF: x ∉ F.
Set U0 to be the term Sorgenfrey_line ∖ F.
We prove the intermediate claim HU0open_in: open_in Sorgenfrey_line Sorgenfrey_topology U0.
We prove the intermediate claim HU0def: U0 = Sorgenfrey_line ∖ F.
Use reflexivity.
rewrite the current goal using HU0def (from left to right).
An exact proof term for the current goal is (open_of_closed_complement Sorgenfrey_line Sorgenfrey_topology F HFcl).
We prove the intermediate claim HU0open: U0 ∈ Sorgenfrey_topology.
An exact proof term for the current goal is (open_in_elem Sorgenfrey_line Sorgenfrey_topology U0 HU0open_in).
We prove the intermediate claim HxU0: x ∈ U0.
Apply setminusI to the current goal.
An exact proof term for the current goal is HxR.
An exact proof term for the current goal is HxnotF.
We prove the intermediate claim Hexb: ∃b ∈ R_lower_limit_basis, x ∈ b ∧ b ⊆ U0.
An exact proof term for the current goal is (generated_topology_local_refine R R_lower_limit_basis U0 x HU0open HxU0).
Apply Hexb to the current goal.
Let b be given.
Assume Hbpair.
We prove the intermediate claim HbB: b ∈ R_lower_limit_basis.
An exact proof term for the current goal is (andEL (b ∈ R_lower_limit_basis) (x ∈ b ∧ b ⊆ U0) Hbpair).
We prove the intermediate claim Hxb: x ∈ b.
An exact proof term for the current goal is (andEL (x ∈ b) (b ⊆ U0) (andER (b ∈ R_lower_limit_basis) (x ∈ b ∧ b ⊆ U0) Hbpair)).
We prove the intermediate claim HbSubU0: b ⊆ U0.
An exact proof term for the current goal is (andER (x ∈ b) (b ⊆ U0) (andER (b ∈ R_lower_limit_basis) (x ∈ b ∧ b ⊆ U0) Hbpair)).
We prove the intermediate claim Hbopen: b ∈ Sorgenfrey_topology.
An exact proof term for the current goal is (generated_topology_contains_basis R R_lower_limit_basis R_lower_limit_basis_is_basis_local b HbB).
We prove the intermediate claim Hexa: ∃a ∈ R, b ∈ {halfopen_interval_left a d|d ∈ R}.
An exact proof term for the current goal is (famunionE R (λa0 : set ⇒ {halfopen_interval_left a0 d|d ∈ R}) b HbB).
Apply Hexa to the current goal.
Let a be given.
Assume Hapair.
We prove the intermediate claim HaR: a ∈ R.
An exact proof term for the current goal is (andEL (a ∈ R) (b ∈ {halfopen_interval_left a d|d ∈ R}) Hapair).
We prove the intermediate claim HbFam: b ∈ {halfopen_interval_left a d|d ∈ R}.
An exact proof term for the current goal is (andER (a ∈ R) (b ∈ {halfopen_interval_left a d|d ∈ R}) Hapair).
We prove the intermediate claim Hexd: ∃d ∈ R, b = halfopen_interval_left a d.
An exact proof term for the current goal is (ReplE R (λd0 : set ⇒ halfopen_interval_left a d0) b HbFam).
Apply Hexd to the current goal.
Let d be given.
Assume Hdpair.
We prove the intermediate claim HdR: d ∈ R.
An exact proof term for the current goal is (andEL (d ∈ R) (b = halfopen_interval_left a d) Hdpair).
We prove the intermediate claim Hbeq: b = halfopen_interval_left a d.
An exact proof term for the current goal is (andER (d ∈ R) (b = halfopen_interval_left a d) Hdpair).
We use b to witness the existential quantifier.
We use (Sorgenfrey_line ∖ b) to witness the existential quantifier.
Apply and5I to the current goal.
An exact proof term for the current goal is Hbopen.
We prove the intermediate claim HeqV: (Sorgenfrey_line ∖ b) = (R ∖ halfopen_interval_left a d).
rewrite the current goal using Hbeq (from left to right).
Use reflexivity.
rewrite the current goal using HeqV (from left to right).
An exact proof term for the current goal is (complement_halfopen_interval_left_in_R_lower_limit_topology a d HaR HdR).
An exact proof term for the current goal is Hxb.
Let y be given.
Assume HyF: y ∈ F.
We will prove y ∈ (Sorgenfrey_line ∖ b).
We prove the intermediate claim HFsubR: F ⊆ Sorgenfrey_line.
An exact proof term for the current goal is (closed_in_subset Sorgenfrey_line Sorgenfrey_topology F HFcl).
We prove the intermediate claim HyR: y ∈ Sorgenfrey_line.
An exact proof term for the current goal is (HFsubR y HyF).
Apply (setminusI Sorgenfrey_line b y HyR) to the current goal.
Assume Hyb: y ∈ b.
We prove the intermediate claim HyU0: y ∈ U0.
An exact proof term for the current goal is (HbSubU0 y Hyb).
We prove the intermediate claim HyNotF: y ∉ F.
An exact proof term for the current goal is (setminusE2 Sorgenfrey_line F y HyU0).
An exact proof term for the current goal is (HyNotF HyF).
Apply Empty_Subq_eq to the current goal.
Let z be given.
Assume Hz: z ∈ b ∩ (Sorgenfrey_line ∖ b).
We will prove z ∈ Empty.
We prove the intermediate claim HzU: z ∈ b.
An exact proof term for the current goal is (binintersectE1 b (Sorgenfrey_line ∖ b) z Hz).
We prove the intermediate claim HzV: z ∈ (Sorgenfrey_line ∖ b).
An exact proof term for the current goal is (binintersectE2 b (Sorgenfrey_line ∖ b) z Hz).
We prove the intermediate claim HznU: z ∉ b.
An exact proof term for the current goal is (setminusE2 Sorgenfrey_line b z HzV).
Apply FalseE to the current goal.
An exact proof term for the current goal is (HznU HzU).
∎