Set X to be the term setprod Sorgenfrey_line Sorgenfrey_line.
Set Tx to be the term Sorgenfrey_plane_topology.
Set L to be the term Sorgenfrey_plane_L.
Set Ta to be the term subspace_topology X Tx L.
Set A to be the term Sorgenfrey_plane_diag_irrational.
Set B to be the term Sorgenfrey_plane_diag_rational.
We prove the intermediate claim HTline: topology_on Sorgenfrey_line Sorgenfrey_topology.
An exact proof term for the current goal is R_lower_limit_topology_is_topology.
We prove the intermediate claim HTx: topology_on X Tx.
We prove the intermediate claim Hdef: Tx = product_topology Sorgenfrey_line Sorgenfrey_topology Sorgenfrey_line Sorgenfrey_topology.
Use reflexivity.
rewrite the current goal using Hdef (from left to right).
An exact proof term for the current goal is (product_topology_is_topology Sorgenfrey_line Sorgenfrey_topology Sorgenfrey_line Sorgenfrey_topology HTline HTline).
We prove the intermediate claim HLcl: closed_in X Tx L.
An exact proof term for the current goal is Sorgenfrey_plane_L_closed.
We prove the intermediate claim HLsubX: L ⊆ X.
An exact proof term for the current goal is (closed_in_subset X Tx L HLcl).
We prove the intermediate claim HTa: topology_on L Ta.
An exact proof term for the current goal is (subspace_topology_is_topology X Tx L HTx HLsubX).
We prove the intermediate claim HAsubL: A ⊆ L.
Let p be given.
Assume HpA: p ∈ A.
We prove the intermediate claim Hexx: ∃x ∈ (Sorgenfrey_line ∖ rational_numbers), p = (x,minus_SNo x).
An exact proof term for the current goal is (ReplE (Sorgenfrey_line ∖ rational_numbers) (λx0 : set ⇒ (x0,minus_SNo x0)) p HpA).
Apply Hexx to the current goal.
Let x be given.
Assume Hxpair.
We prove the intermediate claim HxIrr: x ∈ (Sorgenfrey_line ∖ rational_numbers).
An exact proof term for the current goal is (andEL (x ∈ (Sorgenfrey_line ∖ rational_numbers)) (p = (x,minus_SNo x)) Hxpair).
We prove the intermediate claim Hpeq: p = (x,minus_SNo x).
An exact proof term for the current goal is (andER (x ∈ (Sorgenfrey_line ∖ rational_numbers)) (p = (x,minus_SNo x)) Hxpair).
We prove the intermediate claim HxSline: x ∈ Sorgenfrey_line.
An exact proof term for the current goal is (setminusE1 Sorgenfrey_line rational_numbers x HxIrr).
rewrite the current goal using Hpeq (from left to right).
An exact proof term for the current goal is (ReplI Sorgenfrey_line (λt : set ⇒ (t,minus_SNo t)) x HxSline).
We prove the intermediate claim HBsubL: B ⊆ L.
Let p be given.
Assume HpB: p ∈ B.
We prove the intermediate claim Hexx: ∃x ∈ rational_numbers, p = (x,minus_SNo x).
An exact proof term for the current goal is (ReplE rational_numbers (λx0 : set ⇒ (x0,minus_SNo x0)) p HpB).
Apply Hexx to the current goal.
Let x be given.
Assume Hxpair.
We prove the intermediate claim HxQ: x ∈ rational_numbers.
An exact proof term for the current goal is (andEL (x ∈ rational_numbers) (p = (x,minus_SNo x)) Hxpair).
We prove the intermediate claim Hpeq: p = (x,minus_SNo x).
An exact proof term for the current goal is (andER (x ∈ rational_numbers) (p = (x,minus_SNo x)) Hxpair).
We prove the intermediate claim HxR: x ∈ R.
An exact proof term for the current goal is (rational_numbers_in_R x HxQ).
We prove the intermediate claim HxSline: x ∈ Sorgenfrey_line.
We prove the intermediate claim HSlineDef: Sorgenfrey_line = R.
Use reflexivity.
rewrite the current goal using HSlineDef (from left to right).
An exact proof term for the current goal is HxR.
rewrite the current goal using Hpeq (from left to right).
An exact proof term for the current goal is (ReplI Sorgenfrey_line (λt : set ⇒ (t,minus_SNo t)) x HxSline).
We prove the intermediate claim HBopen: open_in L Ta B.
Apply (iffER (open_in L Ta B) (∃V ∈ Tx, B = V ∩ L) (open_in_subspace_iff X Tx L B HTx HLsubX HBsubL)) to the current goal.
Set Fam to be the term {Sorgenfrey_plane_special_rectangle x (add_SNo x 1) (add_SNo (minus_SNo x) 1)|x ∈ rational_numbers}.
Set V to be the term ⋃ Fam.
We use V to witness the existential quantifier.
Apply andI to the current goal.
We prove the intermediate claim HFamPow: Fam ∈ 𝒫 Tx.
Apply PowerI Tx Fam to the current goal.
Let W be given.
Assume HW: W ∈ Fam.
We will prove W ∈ Tx.
We prove the intermediate claim Hexx: ∃x ∈ rational_numbers, W = Sorgenfrey_plane_special_rectangle x (add_SNo x 1) (add_SNo (minus_SNo x) 1).
An exact proof term for the current goal is (ReplE rational_numbers (λx0 : set ⇒ Sorgenfrey_plane_special_rectangle x0 (add_SNo x0 1) (add_SNo (minus_SNo x0) 1)) W HW).
Apply Hexx to the current goal.
Let x be given.
Assume Hxpair.
We prove the intermediate claim HxQ: x ∈ rational_numbers.
An exact proof term for the current goal is (andEL (x ∈ rational_numbers) (W = Sorgenfrey_plane_special_rectangle x (add_SNo x 1) (add_SNo (minus_SNo x) 1)) Hxpair).
We prove the intermediate claim HWeq: W = Sorgenfrey_plane_special_rectangle x (add_SNo x 1) (add_SNo (minus_SNo x) 1).
An exact proof term for the current goal is (andER (x ∈ rational_numbers) (W = Sorgenfrey_plane_special_rectangle x (add_SNo x 1) (add_SNo (minus_SNo x) 1)) Hxpair).
We prove the intermediate claim HxR: x ∈ R.
An exact proof term for the current goal is (rational_numbers_in_R x HxQ).
We prove the intermediate claim HbR: add_SNo x 1 ∈ R.
An exact proof term for the current goal is (real_add_SNo x HxR 1 real_1).
We prove the intermediate claim HmxR: minus_SNo x ∈ R.
An exact proof term for the current goal is (real_minus_SNo x HxR).
We prove the intermediate claim HdR: add_SNo (minus_SNo x) 1 ∈ R.
An exact proof term for the current goal is (real_add_SNo (minus_SNo x) HmxR 1 real_1).
rewrite the current goal using HWeq (from left to right).
An exact proof term for the current goal is (Sorgenfrey_plane_special_rectangle_open x (add_SNo x 1) (add_SNo (minus_SNo x) 1) HxR HbR HdR).
An exact proof term for the current goal is (topology_union_axiom X Tx HTx Fam HFamPow).
Apply set_ext to the current goal.
Let p be given.
Assume HpB: p ∈ B.
We will prove p ∈ V ∩ L.
We prove the intermediate claim Hexx: ∃x ∈ rational_numbers, p = (x,minus_SNo x).
An exact proof term for the current goal is (ReplE rational_numbers (λx0 : set ⇒ (x0,minus_SNo x0)) p HpB).
Apply Hexx to the current goal.
Let x be given.
Assume Hxpair.
We prove the intermediate claim HxQ: x ∈ rational_numbers.
An exact proof term for the current goal is (andEL (x ∈ rational_numbers) (p = (x,minus_SNo x)) Hxpair).
We prove the intermediate claim Hpeq: p = (x,minus_SNo x).
An exact proof term for the current goal is (andER (x ∈ rational_numbers) (p = (x,minus_SNo x)) Hxpair).
We prove the intermediate claim HxR: x ∈ R.
An exact proof term for the current goal is (rational_numbers_in_R x HxQ).
We prove the intermediate claim HxSline: x ∈ Sorgenfrey_line.
We prove the intermediate claim HSlineDef: Sorgenfrey_line = R.
Use reflexivity.
rewrite the current goal using HSlineDef (from left to right).
An exact proof term for the current goal is HxR.
We prove the intermediate claim HpL: p ∈ L.
rewrite the current goal using Hpeq (from left to right).
An exact proof term for the current goal is (ReplI Sorgenfrey_line (λt : set ⇒ (t,minus_SNo t)) x HxSline).
We prove the intermediate claim HpV: p ∈ V.
rewrite the current goal using Hpeq (from left to right).
Apply (UnionI Fam (x,minus_SNo x) (Sorgenfrey_plane_special_rectangle x (add_SNo x 1) (add_SNo (minus_SNo x) 1))) to the current goal.
We prove the intermediate claim HxS: SNo x.
An exact proof term for the current goal is (real_SNo x HxR).
We prove the intermediate claim HmxR: minus_SNo x ∈ R.
An exact proof term for the current goal is (real_minus_SNo x HxR).
We prove the intermediate claim HmxS: SNo (minus_SNo x).
An exact proof term for the current goal is (real_SNo (minus_SNo x) HmxR).
We prove the intermediate claim HbR: add_SNo x 1 ∈ R.
An exact proof term for the current goal is (real_add_SNo x HxR 1 real_1).
We prove the intermediate claim HdR: add_SNo (minus_SNo x) 1 ∈ R.
An exact proof term for the current goal is (real_add_SNo (minus_SNo x) HmxR 1 real_1).
We prove the intermediate claim Hx0eq: add_SNo x 0 = x.
An exact proof term for the current goal is (add_SNo_0R x HxS).
We prove the intermediate claim Hmx0eq: add_SNo (minus_SNo x) 0 = minus_SNo x.
An exact proof term for the current goal is (add_SNo_0R (minus_SNo x) HmxS).
We prove the intermediate claim Hxlt: add_SNo x 0 < add_SNo x 1.
An exact proof term for the current goal is (add_SNo_Lt2 x 0 1 HxS SNo_0 SNo_1 SNoLt_0_1).
We prove the intermediate claim Hmxlt: add_SNo (minus_SNo x) 0 < add_SNo (minus_SNo x) 1.
An exact proof term for the current goal is (add_SNo_Lt2 (minus_SNo x) 0 1 HmxS SNo_0 SNo_1 SNoLt_0_1).
We prove the intermediate claim Hxltb: x < add_SNo x 1.
rewrite the current goal using Hx0eq (from right to left) at position 1.
An exact proof term for the current goal is Hxlt.
We prove the intermediate claim HmxLtd: (minus_SNo x) < add_SNo (minus_SNo x) 1.
rewrite the current goal using Hmx0eq (from right to left) at position 1.
An exact proof term for the current goal is Hmxlt.
We prove the intermediate claim HxRltb: Rlt x (add_SNo x 1).
An exact proof term for the current goal is (RltI x (add_SNo x 1) HxR HbR Hxltb).
We prove the intermediate claim HmxRltd: Rlt (minus_SNo x) (add_SNo (minus_SNo x) 1).
An exact proof term for the current goal is (RltI (minus_SNo x) (add_SNo (minus_SNo x) 1) HmxR HdR HmxLtd).
We prove the intermediate claim HxU: x ∈ halfopen_interval_left x (add_SNo x 1).
An exact proof term for the current goal is (halfopen_interval_left_leftmem x (add_SNo x 1) HxRltb).
We prove the intermediate claim HxV: (minus_SNo x) ∈ halfopen_interval_left (minus_SNo x) (add_SNo (minus_SNo x) 1).
An exact proof term for the current goal is (halfopen_interval_left_leftmem (minus_SNo x) (add_SNo (minus_SNo x) 1) HmxRltd).
An exact proof term for the current goal is (tuple_2_rectangle_set (halfopen_interval_left x (add_SNo x 1)) (halfopen_interval_left (minus_SNo x) (add_SNo (minus_SNo x) 1)) x (minus_SNo x) HxU HxV).
An exact proof term for the current goal is (ReplI rational_numbers (λx0 : set ⇒ Sorgenfrey_plane_special_rectangle x0 (add_SNo x0 1) (add_SNo (minus_SNo x0) 1)) x HxQ).
An exact proof term for the current goal is (binintersectI V L p HpV HpL).
Let p be given.
Assume HpVL: p ∈ V ∩ L.
We will prove p ∈ B.
We prove the intermediate claim HpV: p ∈ V.
An exact proof term for the current goal is (binintersectE1 V L p HpVL).
We prove the intermediate claim HpL: p ∈ L.
An exact proof term for the current goal is (binintersectE2 V L p HpVL).
We prove the intermediate claim Hext: ∃t ∈ Sorgenfrey_line, p = (t,minus_SNo t).
An exact proof term for the current goal is (ReplE Sorgenfrey_line (λt0 : set ⇒ (t0,minus_SNo t0)) p HpL).
Apply Hext to the current goal.
Let t be given.
Assume Htpair.
We prove the intermediate claim HtSline: t ∈ Sorgenfrey_line.
An exact proof term for the current goal is (andEL (t ∈ Sorgenfrey_line) (p = (t,minus_SNo t)) Htpair).
We prove the intermediate claim Hpeq: p = (t,minus_SNo t).
An exact proof term for the current goal is (andER (t ∈ Sorgenfrey_line) (p = (t,minus_SNo t)) Htpair).
Apply (UnionE_impred Fam p HpV (p ∈ B)) to the current goal.
Let W be given.
Assume HpW: p ∈ W.
Assume HWFam: W ∈ Fam.
We will prove p ∈ B.
We prove the intermediate claim Hexx: ∃x ∈ rational_numbers, W = Sorgenfrey_plane_special_rectangle x (add_SNo x 1) (add_SNo (minus_SNo x) 1).
An exact proof term for the current goal is (ReplE rational_numbers (λx0 : set ⇒ Sorgenfrey_plane_special_rectangle x0 (add_SNo x0 1) (add_SNo (minus_SNo x0) 1)) W HWFam).
Apply Hexx to the current goal.
Let x be given.
Assume Hxpair.
We prove the intermediate claim HxQ: x ∈ rational_numbers.
An exact proof term for the current goal is (andEL (x ∈ rational_numbers) (W = Sorgenfrey_plane_special_rectangle x (add_SNo x 1) (add_SNo (minus_SNo x) 1)) Hxpair).
We prove the intermediate claim HWeq: W = Sorgenfrey_plane_special_rectangle x (add_SNo x 1) (add_SNo (minus_SNo x) 1).
An exact proof term for the current goal is (andER (x ∈ rational_numbers) (W = Sorgenfrey_plane_special_rectangle x (add_SNo x 1) (add_SNo (minus_SNo x) 1)) Hxpair).
We prove the intermediate claim HtR: t ∈ R.
We prove the intermediate claim HSlineDef: Sorgenfrey_line = R.
Use reflexivity.
rewrite the current goal using HSlineDef (from right to left).
An exact proof term for the current goal is HtSline.
We prove the intermediate claim HxR: x ∈ R.
An exact proof term for the current goal is (rational_numbers_in_R x HxQ).
We prove the intermediate claim HbR: add_SNo x 1 ∈ R.
An exact proof term for the current goal is (real_add_SNo x HxR 1 real_1).
We prove the intermediate claim HmxR: minus_SNo x ∈ R.
An exact proof term for the current goal is (real_minus_SNo x HxR).
We prove the intermediate claim HdR: add_SNo (minus_SNo x) 1 ∈ R.
An exact proof term for the current goal is (real_add_SNo (minus_SNo x) HmxR 1 real_1).
We prove the intermediate claim HpInRect: (t,minus_SNo t) ∈ Sorgenfrey_plane_special_rectangle x (add_SNo x 1) (add_SNo (minus_SNo x) 1).
rewrite the current goal using HWeq (from right to left) at position 1.
rewrite the current goal using Hpeq (from right to left) at position 1.
An exact proof term for the current goal is HpW.
We prove the intermediate claim Htx: t = x.
An exact proof term for the current goal is (Sorgenfrey_plane_special_rectangle_L_point x (add_SNo x 1) (add_SNo (minus_SNo x) 1) t HxR HbR HdR HtR HpInRect).
rewrite the current goal using Hpeq (from left to right).
rewrite the current goal using Htx (from left to right).
An exact proof term for the current goal is (ReplI rational_numbers (λx0 : set ⇒ (x0,minus_SNo x0)) x HxQ).
We prove the intermediate claim HBelem: B ∈ Ta.
An exact proof term for the current goal is (open_in_elem L Ta B HBopen).
We prove the intermediate claim HAeq: A = L ∖ B.
Apply set_ext to the current goal.
Let p be given.
Assume HpA: p ∈ A.
We will prove p ∈ L ∖ B.
Apply setminusI to the current goal.
An exact proof term for the current goal is (HAsubL p HpA).
Assume HpB: p ∈ B.
We will prove False.
We prove the intermediate claim HpAB: p ∈ A ∩ B.
An exact proof term for the current goal is (binintersectI A B p HpA HpB).
We prove the intermediate claim HpEmpty: p ∈ Empty.
We prove the intermediate claim HabEmpty: A ∩ B = Empty.
rewrite the current goal using (binintersect_com A B) (from left to right).
An exact proof term for the current goal is Sorgenfrey_plane_diag_disjoint.
rewrite the current goal using HabEmpty (from right to left).
An exact proof term for the current goal is HpAB.
An exact proof term for the current goal is (EmptyE p HpEmpty).
Let p be given.
Assume HpLB: p ∈ L ∖ B.
We will prove p ∈ A.
We prove the intermediate claim HpL: p ∈ L.
An exact proof term for the current goal is (setminusE1 L B p HpLB).
We prove the intermediate claim HpnotB: p ∉ B.
An exact proof term for the current goal is (setminusE2 L B p HpLB).
We prove the intermediate claim Hext: ∃t ∈ Sorgenfrey_line, p = (t,minus_SNo t).
An exact proof term for the current goal is (ReplE Sorgenfrey_line (λt0 : set ⇒ (t0,minus_SNo t0)) p HpL).
Apply Hext to the current goal.
Let t be given.
Assume Htpair.
We prove the intermediate claim HtSline: t ∈ Sorgenfrey_line.
An exact proof term for the current goal is (andEL (t ∈ Sorgenfrey_line) (p = (t,minus_SNo t)) Htpair).
We prove the intermediate claim Hpeq: p = (t,minus_SNo t).
An exact proof term for the current goal is (andER (t ∈ Sorgenfrey_line) (p = (t,minus_SNo t)) Htpair).
Apply (xm (t ∈ rational_numbers)) to the current goal.
Assume HtQ: t ∈ rational_numbers.
Apply FalseE to the current goal.
We will prove False.
We prove the intermediate claim HpB: p ∈ B.
rewrite the current goal using Hpeq (from left to right).
An exact proof term for the current goal is (ReplI rational_numbers (λx0 : set ⇒ (x0,minus_SNo x0)) t HtQ).
An exact proof term for the current goal is (HpnotB HpB).
Assume HtnQ: t ∉ rational_numbers.
We prove the intermediate claim HtIrr: t ∈ (Sorgenfrey_line ∖ rational_numbers).
Apply setminusI to the current goal.
An exact proof term for the current goal is HtSline.
An exact proof term for the current goal is HtnQ.
rewrite the current goal using Hpeq (from left to right).
An exact proof term for the current goal is (ReplI (Sorgenfrey_line ∖ rational_numbers) (λx0 : set ⇒ (x0,minus_SNo x0)) t HtIrr).
We prove the intermediate claim HAclL: closed_in L Ta A.
Apply (closed_inI L Ta A HTa HAsubL) to the current goal.
We use B to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HBelem.
An exact proof term for the current goal is HAeq.
An exact proof term for the current goal is (ex17_2_closed_in_closed_subspace X Tx L A HLcl HAclL).
∎