We will prove ¬ Lindelof_space (setprod Sorgenfrey_line Sorgenfrey_line) Sorgenfrey_plane_topology.
Assume HL: Lindelof_space (setprod Sorgenfrey_line Sorgenfrey_line) Sorgenfrey_plane_topology.
We will prove False.
Set X to be the term setprod Sorgenfrey_line Sorgenfrey_line.
Set Tx to be the term Sorgenfrey_plane_topology.
We prove the intermediate claim HTx: topology_on X Tx.
An exact proof term for the current goal is (andEL (topology_on X Tx) (∀U : set, open_cover X Tx U → ∃V : set, countable_subcollection V U ∧ covers X V) HL).
We prove the intermediate claim HLind: ∀U : set, open_cover X Tx U → ∃V : set, countable_subcollection V U ∧ covers X V.
An exact proof term for the current goal is (andER (topology_on X Tx) (∀U : set, open_cover X Tx U → ∃V : set, countable_subcollection V U ∧ covers X V) HL).
Set L to be the term Sorgenfrey_plane_L.
Set Lcomp to be the term X ∖ L.
Set FamSpec to be the term (⋃a ∈ R⋃b ∈ R{Sorgenfrey_plane_special_rectangle a b d|d ∈ R}).
Set Cover to be the term {Lcomp} ∪ FamSpec.
We prove the intermediate claim Hcover_open: ∀U : set, U ∈ Cover → U ∈ Tx.
Let U be given.
Assume HU: U ∈ Cover.
Apply (binunionE {Lcomp} FamSpec U HU) to the current goal.
Assume HUs: U ∈ {Lcomp}.
We prove the intermediate claim Heq: U = Lcomp.
An exact proof term for the current goal is (SingE Lcomp U HUs).
rewrite the current goal using Heq (from left to right).
We prove the intermediate claim Hcl: closed_in X Tx L.
An exact proof term for the current goal is Sorgenfrey_plane_L_closed.
We prove the intermediate claim Hopen: open_in X Tx (X ∖ L).
An exact proof term for the current goal is (open_of_closed_complement X Tx L Hcl).
An exact proof term for the current goal is (andER (topology_on X Tx) ((X ∖ L) ∈ Tx) Hopen).
Assume HUF: U ∈ FamSpec.
We prove the intermediate claim Hexa: ∃a ∈ R, U ∈ (⋃b ∈ R{Sorgenfrey_plane_special_rectangle a b d|d ∈ R}).
An exact proof term for the current goal is (famunionE R (λa0 : set ⇒ ⋃b ∈ R{Sorgenfrey_plane_special_rectangle a0 b d|d ∈ R}) U HUF).
Apply Hexa to the current goal.
Let a be given.
Assume Hap: a ∈ R ∧ U ∈ (⋃b ∈ R{Sorgenfrey_plane_special_rectangle a b d|d ∈ R}).
We prove the intermediate claim HaR: a ∈ R.
An exact proof term for the current goal is (andEL (a ∈ R) (U ∈ (⋃b ∈ R{Sorgenfrey_plane_special_rectangle a b d|d ∈ R})) Hap).
We prove the intermediate claim HUin: U ∈ (⋃b ∈ R{Sorgenfrey_plane_special_rectangle a b d|d ∈ R}).
An exact proof term for the current goal is (andER (a ∈ R) (U ∈ (⋃b ∈ R{Sorgenfrey_plane_special_rectangle a b d|d ∈ R})) Hap).
We prove the intermediate claim Hexb: ∃b ∈ R, U ∈ {Sorgenfrey_plane_special_rectangle a b d|d ∈ R}.
An exact proof term for the current goal is (famunionE R (λb0 : set ⇒ {Sorgenfrey_plane_special_rectangle a b0 d|d ∈ R}) U HUin).
Apply Hexb to the current goal.
Let b be given.
Assume Hbp: b ∈ R ∧ U ∈ {Sorgenfrey_plane_special_rectangle a b d|d ∈ R}.
We prove the intermediate claim HbR: b ∈ R.
An exact proof term for the current goal is (andEL (b ∈ R) (U ∈ {Sorgenfrey_plane_special_rectangle a b d|d ∈ R}) Hbp).
We prove the intermediate claim HUrepl: U ∈ {Sorgenfrey_plane_special_rectangle a b d|d ∈ R}.
An exact proof term for the current goal is (andER (b ∈ R) (U ∈ {Sorgenfrey_plane_special_rectangle a b d|d ∈ R}) Hbp).
We prove the intermediate claim Hexd: ∃d ∈ R, U = Sorgenfrey_plane_special_rectangle a b d.
An exact proof term for the current goal is (ReplE R (λd0 : set ⇒ Sorgenfrey_plane_special_rectangle a b d0) U HUrepl).
Apply Hexd to the current goal.
Let d be given.
Assume Hdp: d ∈ R ∧ U = Sorgenfrey_plane_special_rectangle a b d.
We prove the intermediate claim HdR: d ∈ R.
An exact proof term for the current goal is (andEL (d ∈ R) (U = Sorgenfrey_plane_special_rectangle a b d) Hdp).
We prove the intermediate claim Heq: U = Sorgenfrey_plane_special_rectangle a b d.
An exact proof term for the current goal is (andER (d ∈ R) (U = Sorgenfrey_plane_special_rectangle a b d) Hdp).
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is (Sorgenfrey_plane_special_rectangle_open a b d HaR HbR HdR).
We prove the intermediate claim Hcover_covers: covers X Cover.
Let p be given.
Assume HpX: p ∈ X.
Apply (xm (p ∈ L)) to the current goal.
Assume HpL: p ∈ L.
We prove the intermediate claim Hexx: ∃x ∈ R, p = (x,minus_SNo x).
An exact proof term for the current goal is (ReplE R (λx0 : set ⇒ (x0,minus_SNo x0)) p HpL).
Apply Hexx to the current goal.
Let x be given.
Assume Hxp: x ∈ R ∧ p = (x,minus_SNo x).
We prove the intermediate claim HxR: x ∈ R.
An exact proof term for the current goal is (andEL (x ∈ R) (p = (x,minus_SNo x)) Hxp).
We prove the intermediate claim Hpeq: p = (x,minus_SNo x).
An exact proof term for the current goal is (andER (x ∈ R) (p = (x,minus_SNo x)) Hxp).
Set b to be the term add_SNo x 1.
Set d to be the term add_SNo (minus_SNo x) 1.
We prove the intermediate claim HbR: b ∈ R.
An exact proof term for the current goal is (real_add_SNo x HxR 1 real_1).
We prove the intermediate claim HdR: d ∈ R.
An exact proof term for the current goal is (real_add_SNo (minus_SNo x) (real_minus_SNo x HxR) 1 real_1).
Set U0 to be the term Sorgenfrey_plane_special_rectangle x b d.
We prove the intermediate claim HU0inFam: U0 ∈ FamSpec.
We will prove U0 ∈ (⋃a ∈ R⋃b0 ∈ R{Sorgenfrey_plane_special_rectangle a b0 d0|d0 ∈ R}).
Apply (famunionI R (λa0 : set ⇒ ⋃b0 ∈ R{Sorgenfrey_plane_special_rectangle a0 b0 d0|d0 ∈ R}) x) to the current goal.
An exact proof term for the current goal is HxR.
We will prove U0 ∈ (⋃b0 ∈ R{Sorgenfrey_plane_special_rectangle x b0 d0|d0 ∈ R}).
Apply (famunionI R (λb0 : set ⇒ {Sorgenfrey_plane_special_rectangle x b0 d0|d0 ∈ R}) b) to the current goal.
An exact proof term for the current goal is HbR.
We will prove U0 ∈ {Sorgenfrey_plane_special_rectangle x b d0|d0 ∈ R}.
An exact proof term for the current goal is (ReplI R (λd0 : set ⇒ Sorgenfrey_plane_special_rectangle x b d0) d HdR).
We prove the intermediate claim HU0inC: U0 ∈ Cover.
An exact proof term for the current goal is (binunionI2 {Lcomp} FamSpec U0 HU0inFam).
We prove the intermediate claim HpU0: p ∈ U0.
rewrite the current goal using Hpeq (from left to right).
We prove the intermediate claim HU0eq: U0 = rectangle_set (halfopen_interval_left x b) (halfopen_interval_left (minus_SNo x) d).
Use reflexivity.
rewrite the current goal using HU0eq (from left to right).
rewrite the current goal using rectangle_set_def (from left to right).
We will prove (x,minus_SNo x) ∈ setprod (halfopen_interval_left x b) (halfopen_interval_left (minus_SNo x) d).
Apply tuple_2_setprod_by_pair_Sigma 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 Hx_lt_bS: x < b.
rewrite the current goal using (add_SNo_0R x HxS) (from right to left) at position 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 Hx_lt_bR: Rlt x b.
An exact proof term for the current goal is (RltI x b HxR HbR Hx_lt_bS).
An exact proof term for the current goal is (halfopen_interval_left_leftmem x b Hx_lt_bR).
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 Hmx_lt_dS: (minus_SNo x) < d.
rewrite the current goal using (add_SNo_0R (minus_SNo x) HmxS) (from right to left) at position 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 Hmx_lt_dR: Rlt (minus_SNo x) d.
An exact proof term for the current goal is (RltI (minus_SNo x) d HmxR HdR Hmx_lt_dS).
An exact proof term for the current goal is (halfopen_interval_left_leftmem (minus_SNo x) d Hmx_lt_dR).
We use U0 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HU0inC.
An exact proof term for the current goal is HpU0.
Assume HpnotL: p ∉ L.
We prove the intermediate claim HpLcomp: p ∈ Lcomp.
Apply setminusI to the current goal.
An exact proof term for the current goal is HpX.
An exact proof term for the current goal is HpnotL.
We prove the intermediate claim HLcompC: Lcomp ∈ Cover.
An exact proof term for the current goal is (binunionI1 {Lcomp} FamSpec Lcomp (SingI Lcomp)).
We use Lcomp to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HLcompC.
An exact proof term for the current goal is HpLcomp.
We prove the intermediate claim Hcover: open_cover X Tx Cover.
We will prove (∀u : set, u ∈ Cover → u ∈ Tx) ∧ covers X Cover.
Apply andI to the current goal.
An exact proof term for the current goal is Hcover_open.
An exact proof term for the current goal is Hcover_covers.
We prove the intermediate claim HexV: ∃V : set, countable_subcollection V Cover ∧ covers X V.
An exact proof term for the current goal is (HLind Cover Hcover).
Apply HexV to the current goal.
Let V be given.
Assume HVp: countable_subcollection V Cover ∧ covers X V.
We prove the intermediate claim HVcount: countable_subcollection V Cover.
An exact proof term for the current goal is (andEL (countable_subcollection V Cover) (covers X V) HVp).
We prove the intermediate claim HVcov: covers X V.
An exact proof term for the current goal is (andER (countable_subcollection V Cover) (covers X V) HVp).
Set pick to be the term λx : set ⇒ Eps_i (λU0 : set ⇒ U0 ∈ V ∧ (x,minus_SNo x) ∈ U0).
We prove the intermediate claim Hpick_spec: ∀x : set, x ∈ R → pick x ∈ V ∧ (x,minus_SNo x) ∈ pick x.
Let x be given.
Assume HxR: x ∈ R.
We prove the intermediate claim HpxX: (x,minus_SNo x) ∈ X.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma R R x (minus_SNo x) HxR (real_minus_SNo x HxR)).
We prove the intermediate claim Hp_in_cov: ∃U0 : set, U0 ∈ V ∧ (x,minus_SNo x) ∈ U0.
An exact proof term for the current goal is (HVcov (x,minus_SNo x) HpxX).
Apply Hp_in_cov to the current goal.
Let U0 be given.
Assume HU0pair: U0 ∈ V ∧ (x,minus_SNo x) ∈ U0.
An exact proof term for the current goal is (Eps_i_ax (λU1 : set ⇒ U1 ∈ V ∧ (x,minus_SNo x) ∈ U1) U0 HU0pair).
We prove the intermediate claim Hpick_inj: inj R V pick.
Apply (injI R V pick) to the current goal.
Let x be given.
Assume HxR: x ∈ R.
An exact proof term for the current goal is (andEL (pick x ∈ V) ((x,minus_SNo x) ∈ pick x) (Hpick_spec x HxR)).
Let x1 be given.
Assume Hx1R: x1 ∈ R.
Let x2 be given.
Assume Hx2R: x2 ∈ R.
Assume Heq: pick x1 = pick x2.
We will prove x1 = x2.
We prove the intermediate claim Hmem1: (x1,minus_SNo x1) ∈ pick x1.
An exact proof term for the current goal is (andER (pick x1 ∈ V) ((x1,minus_SNo x1) ∈ pick x1) (Hpick_spec x1 Hx1R)).
We prove the intermediate claim Hmem2: (x2,minus_SNo x2) ∈ pick x2.
An exact proof term for the current goal is (andER (pick x2 ∈ V) ((x2,minus_SNo x2) ∈ pick x2) (Hpick_spec x2 Hx2R)).
We prove the intermediate claim Hmem1p: (x1,minus_SNo x1) ∈ pick x2.
rewrite the current goal using Heq (from right to left) at position 1.
An exact proof term for the current goal is Hmem1.
We prove the intermediate claim Hboth: (x1,minus_SNo x1) ∈ pick x2 ∧ (x2,minus_SNo x2) ∈ pick x2.
Apply andI to the current goal.
An exact proof term for the current goal is Hmem1p.
An exact proof term for the current goal is Hmem2.
We prove the intermediate claim HVsub: V ⊆ Cover.
An exact proof term for the current goal is (andEL (V ⊆ Cover) (countable_set V) HVcount).
We prove the intermediate claim HcoverU: pick x2 ∈ Cover.
Apply HVsub to the current goal.
An exact proof term for the current goal is (andEL (pick x2 ∈ V) ((x2,minus_SNo x2) ∈ pick x2) (Hpick_spec x2 Hx2R)).
Apply (binunionE {Lcomp} FamSpec (pick x2) HcoverU) to the current goal.
Assume Hsing: pick x2 ∈ {Lcomp}.
We prove the intermediate claim HeqL: pick x2 = Lcomp.
An exact proof term for the current goal is (SingE Lcomp (pick x2) Hsing).
Apply FalseE to the current goal.
We prove the intermediate claim Hmem2L: (x2,minus_SNo x2) ∈ Lcomp.
rewrite the current goal using HeqL (from right to left) at position 1.
An exact proof term for the current goal is Hmem2.
An exact proof term for the current goal is (setminusE2 X L (x2,minus_SNo x2) Hmem2L (ReplI R (λx0 : set ⇒ (x0,minus_SNo x0)) x2 Hx2R)).
Assume Hfam: pick x2 ∈ FamSpec.
We prove the intermediate claim Hexa: ∃a ∈ R, pick x2 ∈ (⋃b0 ∈ R{Sorgenfrey_plane_special_rectangle a b0 d0|d0 ∈ R}).
An exact proof term for the current goal is (famunionE R (λa0 : set ⇒ ⋃b0 ∈ R{Sorgenfrey_plane_special_rectangle a0 b0 d0|d0 ∈ R}) (pick x2) Hfam).
Apply Hexa to the current goal.
Let a be given.
Assume Hap: a ∈ R ∧ pick x2 ∈ (⋃b0 ∈ R{Sorgenfrey_plane_special_rectangle a b0 d0|d0 ∈ R}).
We prove the intermediate claim HaR: a ∈ R.
An exact proof term for the current goal is (andEL (a ∈ R) (pick x2 ∈ (⋃b0 ∈ R{Sorgenfrey_plane_special_rectangle a b0 d0|d0 ∈ R})) Hap).
We prove the intermediate claim HUin: pick x2 ∈ (⋃b0 ∈ R{Sorgenfrey_plane_special_rectangle a b0 d0|d0 ∈ R}).
An exact proof term for the current goal is (andER (a ∈ R) (pick x2 ∈ (⋃b0 ∈ R{Sorgenfrey_plane_special_rectangle a b0 d0|d0 ∈ R})) Hap).
We prove the intermediate claim Hexb: ∃b0 ∈ R, pick x2 ∈ {Sorgenfrey_plane_special_rectangle a b0 d0|d0 ∈ R}.
An exact proof term for the current goal is (famunionE R (λb0 : set ⇒ {Sorgenfrey_plane_special_rectangle a b0 d0|d0 ∈ R}) (pick x2) HUin).
Apply Hexb to the current goal.
Let b be given.
Assume Hbp: b ∈ R ∧ pick x2 ∈ {Sorgenfrey_plane_special_rectangle a b d0|d0 ∈ R}.
We prove the intermediate claim HbR2: b ∈ R.
An exact proof term for the current goal is (andEL (b ∈ R) (pick x2 ∈ {Sorgenfrey_plane_special_rectangle a b d0|d0 ∈ R}) Hbp).
We prove the intermediate claim HUrepl: pick x2 ∈ {Sorgenfrey_plane_special_rectangle a b d0|d0 ∈ R}.
An exact proof term for the current goal is (andER (b ∈ R) (pick x2 ∈ {Sorgenfrey_plane_special_rectangle a b d0|d0 ∈ R}) Hbp).
We prove the intermediate claim Hexd: ∃d ∈ R, pick x2 = Sorgenfrey_plane_special_rectangle a b d.
An exact proof term for the current goal is (ReplE R (λd0 : set ⇒ Sorgenfrey_plane_special_rectangle a b d0) (pick x2) HUrepl).
Apply Hexd to the current goal.
Let d be given.
Assume Hdp: d ∈ R ∧ pick x2 = Sorgenfrey_plane_special_rectangle a b d.
We prove the intermediate claim HdR2: d ∈ R.
An exact proof term for the current goal is (andEL (d ∈ R) (pick x2 = Sorgenfrey_plane_special_rectangle a b d) Hdp).
We prove the intermediate claim HeqU: pick x2 = Sorgenfrey_plane_special_rectangle a b d.
An exact proof term for the current goal is (andER (d ∈ R) (pick x2 = Sorgenfrey_plane_special_rectangle a b d) Hdp).
We prove the intermediate claim Hp1inPick: (x1,minus_SNo x1) ∈ pick x2.
An exact proof term for the current goal is (andEL ((x1,minus_SNo x1) ∈ pick x2) ((x2,minus_SNo x2) ∈ pick x2) Hboth).
We prove the intermediate claim Hp1inRect: (x1,minus_SNo x1) ∈ Sorgenfrey_plane_special_rectangle a b d.
rewrite the current goal using HeqU (from right to left) at position 1.
An exact proof term for the current goal is Hp1inPick.
We prove the intermediate claim Hp2inRect: (x2,minus_SNo x2) ∈ Sorgenfrey_plane_special_rectangle a b d.
rewrite the current goal using HeqU (from right to left) at position 1.
An exact proof term for the current goal is Hmem2.
We prove the intermediate claim Hx1eq: x1 = a.
An exact proof term for the current goal is (Sorgenfrey_plane_special_rectangle_L_point a b d x1 HaR HbR2 HdR2 Hx1R Hp1inRect).
We prove the intermediate claim Hx2eq: x2 = a.
An exact proof term for the current goal is (Sorgenfrey_plane_special_rectangle_L_point a b d x2 HaR HbR2 HdR2 Hx2R Hp2inRect).
rewrite the current goal using Hx1eq (from left to right).
rewrite the current goal using Hx2eq (from left to right).
Use reflexivity.
We prove the intermediate claim HinjRV: atleastp R V.
We will prove ∃f : set → set, inj R V f.
We use pick to witness the existential quantifier.
An exact proof term for the current goal is Hpick_inj.
We prove the intermediate claim HVOmega: atleastp V ω.
We prove the intermediate claim HcountV: countable_set V.
An exact proof term for the current goal is (andER (V ⊆ Cover) (countable_set V) HVcount).
An exact proof term for the current goal is HcountV.
We prove the intermediate claim HcountR: atleastp R ω.
An exact proof term for the current goal is (atleastp_tra R V ω HinjRV HVOmega).
An exact proof term for the current goal is (form100_22_real_uncountable_atleastp HcountR).
∎