We will prove completely_regular_space Sorgenfrey_line Sorgenfrey_topology.
Set X to be the term Sorgenfrey_line.
Set Tx to be the term Sorgenfrey_topology.
We prove the intermediate claim Hreg: regular_space X Tx.
An exact proof term for the current goal is Sorgenfrey_line_regular.
We prove the intermediate claim HTx: topology_on X Tx.
An exact proof term for the current goal is (regular_space_topology_on X Tx Hreg).
We prove the intermediate claim Hone: one_point_sets_closed X Tx.
An exact proof term for the current goal is (andEL (one_point_sets_closed X Tx) (∀x : set, x ∈ X → ∀F : set, closed_in X Tx F → x ∉ F → ∃U V : set, U ∈ Tx ∧ V ∈ Tx ∧ x ∈ U ∧ F ⊆ V ∧ U ∩ V = Empty) Hreg).
We will prove topology_on X Tx ∧ (one_point_sets_closed X Tx ∧ ∀x : set, x ∈ X → ∀F : set, closed_in X Tx F → x ∉ F → ∃f : set, continuous_map X Tx R R_standard_topology f ∧ apply_fun f x = 0 ∧ ∀y : set, y ∈ F → apply_fun f y = 1).
Apply andI to the current goal.
An exact proof term for the current goal is HTx.
Apply andI to the current goal.
An exact proof term for the current goal is Hone.
Let x be given.
Assume HxX: x ∈ X.
Let F be given.
Assume HFcl: closed_in X Tx F.
Assume HxnotF: x ∉ F.
We will prove ∃f : set, continuous_map X Tx R R_standard_topology f ∧ apply_fun f x = 0 ∧ ∀y : set, y ∈ F → apply_fun f y = 1.
We prove the intermediate claim HFsubX: F ⊆ X.
An exact proof term for the current goal is (closed_in_subset X Tx F HFcl).
Set U0 to be the term X ∖ F.
We prove the intermediate claim HU0def: U0 = X ∖ F.
Use reflexivity.
We prove the intermediate claim HU0open_in: open_in X Tx U0.
rewrite the current goal using HU0def (from left to right).
An exact proof term for the current goal is (open_of_closed_complement X Tx F HFcl).
We prove the intermediate claim HU0open: U0 ∈ Tx.
An exact proof term for the current goal is (open_in_elem X Tx U0 HU0open_in).
We prove the intermediate claim HxU0: x ∈ U0.
rewrite the current goal using HU0def (from left to right).
An exact proof term for the current goal is (setminusI X F x HxX 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 ∈ Tx.
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).
Set A to be the term b.
Set B to be the term X ∖ b.
We prove the intermediate claim HAdef: A = b.
Use reflexivity.
We prove the intermediate claim HBdef: B = X ∖ b.
Use reflexivity.
We prove the intermediate claim HbSubX: b ⊆ X.
An exact proof term for the current goal is (topology_elem_subset X Tx b HTx Hbopen).
We prove the intermediate claim HAbSubX: A ⊆ X.
rewrite the current goal using HAdef (from left to right).
An exact proof term for the current goal is HbSubX.
We prove the intermediate claim HBsubX: B ⊆ X.
rewrite the current goal using HBdef (from left to right).
An exact proof term for the current goal is (setminus_Subq X b).
We prove the intermediate claim HAopen: A ∈ Tx.
rewrite the current goal using HAdef (from left to right).
An exact proof term for the current goal is Hbopen.
We prove the intermediate claim HBopen: B ∈ Tx.
rewrite the current goal using HBdef (from left to right).
rewrite the current goal using Hbeq (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).
We prove the intermediate claim HclA: closed_in X Tx A.
Apply (closed_inI X Tx A) to the current goal.
An exact proof term for the current goal is HTx.
An exact proof term for the current goal is HAbSubX.
We use B to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HBopen.
rewrite the current goal using HAdef (from left to right).
rewrite the current goal using HBdef (from left to right).
rewrite the current goal using (setminus_setminus_eq X b HbSubX) (from left to right).
Use reflexivity.
We prove the intermediate claim HclB: closed_in X Tx B.
Apply (closed_inI X Tx B) to the current goal.
An exact proof term for the current goal is HTx.
An exact proof term for the current goal is HBsubX.
We use A to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HAopen.
rewrite the current goal using HBdef (from left to right).
rewrite the current goal using HAdef (from left to right).
Use reflexivity.
We prove the intermediate claim HABeq: A ∪ B = X.
Apply set_ext to the current goal.
Let z be given.
Assume Hz: z ∈ A ∪ B.
Apply (binunionE A B z Hz) to the current goal.
Assume HzA: z ∈ A.
An exact proof term for the current goal is (HAbSubX z HzA).
Assume HzB: z ∈ B.
We prove the intermediate claim HzB': z ∈ X ∖ b.
rewrite the current goal using HBdef (from right to left).
An exact proof term for the current goal is HzB.
An exact proof term for the current goal is (setminusE1 X b z HzB').
Let z be given.
Assume HzX: z ∈ X.
Apply (xm (z ∈ A)) to the current goal.
Assume HzA: z ∈ A.
An exact proof term for the current goal is (binunionI1 A B z HzA).
Assume HznotA: z ∉ A.
We prove the intermediate claim Hznotb: z ∉ b.
rewrite the current goal using HAdef (from right to left).
An exact proof term for the current goal is HznotA.
We prove the intermediate claim HzB: z ∈ B.
rewrite the current goal using HBdef (from left to right).
An exact proof term for the current goal is (setminusI X b z HzX Hznotb).
An exact proof term for the current goal is (binunionI2 A B z HzB).
Set f0 to be the term const_fun A 0.
Set g1 to be the term const_fun B 1.
We prove the intermediate claim HRtop: topology_on R R_standard_topology.
An exact proof term for the current goal is R_standard_topology_is_topology.
We prove the intermediate claim H0R: 0 ∈ R.
An exact proof term for the current goal is real_0.
We prove the intermediate claim H1R: 1 ∈ R.
An exact proof term for the current goal is real_1.
We prove the intermediate claim HTA: topology_on A (subspace_topology X Tx A).
An exact proof term for the current goal is (subspace_topology_is_topology X Tx A HTx HAbSubX).
We prove the intermediate claim HTB: topology_on B (subspace_topology X Tx B).
An exact proof term for the current goal is (subspace_topology_is_topology X Tx B HTx HBsubX).
We prove the intermediate claim Hf0: continuous_map A (subspace_topology X Tx A) R R_standard_topology f0.
An exact proof term for the current goal is (const_fun_continuous A (subspace_topology X Tx A) R R_standard_topology 0 HTA HRtop H0R).
We prove the intermediate claim Hg1: continuous_map B (subspace_topology X Tx B) R R_standard_topology g1.
An exact proof term for the current goal is (const_fun_continuous B (subspace_topology X Tx B) R R_standard_topology 1 HTB HRtop H1R).
We prove the intermediate claim Hagree: ∀z : set, z ∈ (A ∩ B) → apply_fun f0 z = apply_fun g1 z.
Let z be given.
Assume Hz: z ∈ (A ∩ B).
We will prove apply_fun f0 z = apply_fun g1 z.
Apply FalseE to the current goal.
We will prove False.
We prove the intermediate claim HzA: z ∈ A.
An exact proof term for the current goal is (binintersectE1 A B z Hz).
We prove the intermediate claim HzB: z ∈ B.
An exact proof term for the current goal is (binintersectE2 A B z Hz).
We prove the intermediate claim Hzb: z ∈ b.
rewrite the current goal using HAdef (from right to left).
An exact proof term for the current goal is HzA.
We prove the intermediate claim HzB': z ∈ X ∖ b.
rewrite the current goal using HBdef (from right to left).
An exact proof term for the current goal is HzB.
We prove the intermediate claim Hznotb: z ∉ b.
An exact proof term for the current goal is (setminusE2 X b z HzB').
An exact proof term for the current goal is (Hznotb Hzb).
Apply (pasting_lemma X A B R Tx R_standard_topology f0 g1 HTx HclA HclB HABeq Hf0 Hg1 Hagree) to the current goal.
Let h be given.
Assume Hhpack.
We use h to witness the existential quantifier.
We will prove continuous_map X Tx R R_standard_topology h ∧ apply_fun h x = 0 ∧ ∀y : set, y ∈ F → apply_fun h y = 1.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is (andEL (continuous_map X Tx R R_standard_topology h) ((∀z : set, z ∈ A → apply_fun h z = apply_fun f0 z) ∧ (∀z : set, z ∈ B → apply_fun h z = apply_fun g1 z)) Hhpack).
We prove the intermediate claim Hrest: (∀z : set, z ∈ A → apply_fun h z = apply_fun f0 z) ∧ (∀z : set, z ∈ B → apply_fun h z = apply_fun g1 z).
An exact proof term for the current goal is (andER (continuous_map X Tx R R_standard_topology h) ((∀z : set, z ∈ A → apply_fun h z = apply_fun f0 z) ∧ (∀z : set, z ∈ B → apply_fun h z = apply_fun g1 z)) Hhpack).
We prove the intermediate claim HhA: ∀z : set, z ∈ A → apply_fun h z = apply_fun f0 z.
An exact proof term for the current goal is (andEL (∀z : set, z ∈ A → apply_fun h z = apply_fun f0 z) (∀z : set, z ∈ B → apply_fun h z = apply_fun g1 z) Hrest).
We prove the intermediate claim HxA: x ∈ A.
rewrite the current goal using HAdef (from left to right).
An exact proof term for the current goal is Hxb.
We prove the intermediate claim Hhx: apply_fun h x = apply_fun f0 x.
An exact proof term for the current goal is (HhA x HxA).
rewrite the current goal using Hhx (from left to right).
An exact proof term for the current goal is (const_fun_apply A 0 x HxA).
Let y be given.
Assume HyF: y ∈ F.
We will prove apply_fun h y = 1.
We prove the intermediate claim Hrest: (∀z : set, z ∈ A → apply_fun h z = apply_fun f0 z) ∧ (∀z : set, z ∈ B → apply_fun h z = apply_fun g1 z).
An exact proof term for the current goal is (andER (continuous_map X Tx R R_standard_topology h) ((∀z : set, z ∈ A → apply_fun h z = apply_fun f0 z) ∧ (∀z : set, z ∈ B → apply_fun h z = apply_fun g1 z)) Hhpack).
We prove the intermediate claim HhB: ∀z : set, z ∈ B → apply_fun h z = apply_fun g1 z.
An exact proof term for the current goal is (andER (∀z : set, z ∈ A → apply_fun h z = apply_fun f0 z) (∀z : set, z ∈ B → apply_fun h z = apply_fun g1 z) Hrest).
We prove the intermediate claim HyX: y ∈ X.
An exact proof term for the current goal is (HFsubX y HyF).
We prove the intermediate claim HynA: y ∉ A.
Assume HyA: y ∈ A.
We prove the intermediate claim Hyb: y ∈ b.
rewrite the current goal using HAdef (from right to left).
An exact proof term for the current goal is HyA.
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 HynF: y ∉ F.
An exact proof term for the current goal is (setminusE2 X F y HyU0).
Apply FalseE to the current goal.
We will prove False.
An exact proof term for the current goal is (HynF HyF).
We prove the intermediate claim HyB: y ∈ B.
rewrite the current goal using HBdef (from left to right).
An exact proof term for the current goal is (setminusI X b y HyX HynA).
We prove the intermediate claim Hhy: apply_fun h y = apply_fun g1 y.
An exact proof term for the current goal is (HhB y HyB).
rewrite the current goal using Hhy (from left to right).
An exact proof term for the current goal is (const_fun_apply B 1 y HyB).
∎