We will prove subspace_topology (setprod Sorgenfrey_line Sorgenfrey_line) Sorgenfrey_plane_topology Sorgenfrey_plane_L = discrete_topology Sorgenfrey_plane_L.
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.
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 HsingleIn: ∀b ∈ singleton_basis L, b ∈ Ta.
Let b be given.
Assume Hb: b ∈ singleton_basis L.
Apply (ReplE_impred L (λx0 : set ⇒ {x0}) b Hb) to the current goal.
Let p be given.
Assume HpL.
Assume Hbeq: b = {p}.
We prove the intermediate claim HsingSub: {p} ⊆ L.
An exact proof term for the current goal is (singleton_subset p L HpL).
We prove the intermediate claim Hop: open_in L Ta {p}.
Apply (iffER (open_in L Ta {p}) (∃V ∈ Tx, {p} = V ∩ L) (open_in_subspace_iff X Tx L {p} HTx HLsubX HsingSub)) to the current goal.
We prove the intermediate claim Hexx: ∃x ∈ Sorgenfrey_line, p = (x,minus_SNo x).
An exact proof term for the current goal is (ReplE Sorgenfrey_line (λx0 : set ⇒ (x0,minus_SNo x0)) p HpL).
Apply Hexx to the current goal.
Let x be given.
Assume Hxpair.
We prove the intermediate claim HxSline: x ∈ Sorgenfrey_line.
An exact proof term for the current goal is (andEL (x ∈ Sorgenfrey_line) (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) (p = (x,minus_SNo x)) Hxpair).
We prove the intermediate claim HxR: x ∈ 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 HxSline.
Set b0 to be the term add_SNo x 1.
Set d0 to be the term add_SNo (minus_SNo x) 1.
Set V0 to be the term Sorgenfrey_plane_special_rectangle x b0 d0.
We prove the intermediate claim Hb0R: b0 ∈ 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 Hd0R: d0 ∈ R.
An exact proof term for the current goal is (real_add_SNo (minus_SNo x) HmxR 1 real_1).
We use V0 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (Sorgenfrey_plane_special_rectangle_open x b0 d0 HxR Hb0R Hd0R).
Apply set_ext to the current goal.
Let y be given.
Assume Hy: y ∈ {p}.
We will prove y ∈ V0 ∩ L.
We prove the intermediate claim Hyeq: y = p.
An exact proof term for the current goal is (SingE p y Hy).
rewrite the current goal using Hyeq (from left to right).
Apply binintersectI to the current goal.
rewrite the current goal using Hpeq (from left to right).
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 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 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 < b0.
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) < d0.
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 b0.
An exact proof term for the current goal is (RltI x b0 HxR Hb0R Hxltb).
We prove the intermediate claim HmxRltd: Rlt (minus_SNo x) d0.
An exact proof term for the current goal is (RltI (minus_SNo x) d0 HmxR Hd0R Hmxltd).
We prove the intermediate claim HxU: x ∈ halfopen_interval_left x b0.
An exact proof term for the current goal is (halfopen_interval_left_leftmem x b0 HxRltb).
We prove the intermediate claim HxV: (minus_SNo x) ∈ halfopen_interval_left (minus_SNo x) d0.
An exact proof term for the current goal is (halfopen_interval_left_leftmem (minus_SNo x) d0 HmxRltd).
We prove the intermediate claim HdefRect: Sorgenfrey_plane_special_rectangle x b0 d0 = rectangle_set (halfopen_interval_left x b0) (halfopen_interval_left (minus_SNo x) d0).
Use reflexivity.
rewrite the current goal using HdefRect (from left to right).
rewrite the current goal using rectangle_set_def (from left to right).
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma (halfopen_interval_left x b0) (halfopen_interval_left (minus_SNo x) d0) x (minus_SNo x) HxU HxV).
An exact proof term for the current goal is HpL.
Let y be given.
Assume Hy: y ∈ V0 ∩ L.
We will prove y ∈ {p}.
We prove the intermediate claim HyL: y ∈ L.
An exact proof term for the current goal is (binintersectE2 V0 L y Hy).
We prove the intermediate claim Hexy: ∃t ∈ Sorgenfrey_line, y = (t,minus_SNo t).
An exact proof term for the current goal is (ReplE Sorgenfrey_line (λt0 : set ⇒ (t0,minus_SNo t0)) y HyL).
Apply Hexy 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) (y = (t,minus_SNo t)) Htpair).
We prove the intermediate claim Hyeq: y = (t,minus_SNo t).
An exact proof term for the current goal is (andER (t ∈ Sorgenfrey_line) (y = (t,minus_SNo t)) Htpair).
We prove the intermediate claim HyV0: y ∈ V0.
An exact proof term for the current goal is (binintersectE1 V0 L y Hy).
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 HpInRect: (t,minus_SNo t) ∈ V0.
rewrite the current goal using Hyeq (from right to left).
An exact proof term for the current goal is HyV0.
We prove the intermediate claim Htx: t = x.
An exact proof term for the current goal is (Sorgenfrey_plane_special_rectangle_L_point x b0 d0 t HxR Hb0R Hd0R HtR HpInRect).
We prove the intermediate claim HyEqP: y = p.
rewrite the current goal using Hyeq (from left to right).
rewrite the current goal using Htx (from left to right).
rewrite the current goal using Hpeq (from right to left).
Use reflexivity.
rewrite the current goal using HyEqP (from left to right).
An exact proof term for the current goal is (SingI p).
We prove the intermediate claim HsingElem: {p} ∈ Ta.
An exact proof term for the current goal is (open_in_elem L Ta {p} Hop).
rewrite the current goal using Hbeq (from left to right).
An exact proof term for the current goal is HsingElem.
We prove the intermediate claim HsingleBasis: basis_on L (singleton_basis L).
An exact proof term for the current goal is (singleton_basis_is_basis L).
We prove the intermediate claim HdTop: discrete_topology L ⊆ Ta.
We prove the intermediate claim HgenSub: finer_than Ta (generated_topology L (singleton_basis L)).
An exact proof term for the current goal is (generated_topology_finer L (singleton_basis L) Ta HsingleBasis HTa HsingleIn).
We prove the intermediate claim HgenEq: generated_topology L (singleton_basis L) = discrete_topology L.
An exact proof term for the current goal is (generated_topology_singletons_discrete L).
rewrite the current goal using HgenEq (from right to left).
An exact proof term for the current goal is HgenSub.
We prove the intermediate claim HTaSub: Ta ⊆ discrete_topology L.
We prove the intermediate claim HTaPow: Ta ⊆ 𝒫 L.
An exact proof term for the current goal is (topology_subset_axiom L Ta HTa).
An exact proof term for the current goal is HTaPow.
Apply set_ext to the current goal.
An exact proof term for the current goal is HTaSub.
An exact proof term for the current goal is HdTop.
∎