Let X and Tx be given.
Assume Hmet: metrizable X Tx.
Assume HL: Lindelof_space X Tx.
Apply Hmet to the current goal.
Let d be given.
Assume Hdpair: metric_on X d ∧ metric_topology X d = Tx.
We prove the intermediate claim Hm: metric_on X d.
An exact proof term for the current goal is (andEL (metric_on X d) (metric_topology X d = Tx) Hdpair).
We prove the intermediate claim HTdef: metric_topology X d = Tx.
An exact proof term for the current goal is (andER (metric_on X d) (metric_topology X d = Tx) Hdpair).
We prove the intermediate claim HLtop: 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 HLprop: ∀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 BallCover to be the term λN : set ⇒ {open_ball X d x (eps_ N)|x ∈ X} of type set → set.
Set Vsel to be the term λN : set ⇒ Eps_i (λV : set ⇒ countable_subcollection V (BallCover N) ∧ covers X V) of type set → set.
We prove the intermediate claim HVsel_spec: ∀N : set, N ∈ ω → countable_subcollection (Vsel N) (BallCover N) ∧ covers X (Vsel N).
Let N be given.
Assume HNomega: N ∈ ω.
We will prove countable_subcollection (Vsel N) (BallCover N) ∧ covers X (Vsel N).
We prove the intermediate claim HepsR: eps_ N ∈ R.
An exact proof term for the current goal is (SNoS_omega_real (eps_ N) (SNo_eps_SNoS_omega N HNomega)).
We prove the intermediate claim HepsPosS: 0 < eps_ N.
An exact proof term for the current goal is (SNo_eps_pos N HNomega).
We prove the intermediate claim HepsPos: Rlt 0 (eps_ N).
An exact proof term for the current goal is (RltI 0 (eps_ N) real_0 HepsR HepsPosS).
We prove the intermediate claim HTx: topology_on X Tx.
An exact proof term for the current goal is HLtop.
We prove the intermediate claim HTm: topology_on X (metric_topology X d).
An exact proof term for the current goal is (metric_topology_is_topology X d Hm).
We prove the intermediate claim Hcover: open_cover X Tx (BallCover N).
We will prove (∀u : set, u ∈ BallCover N → u ∈ Tx) ∧ covers X (BallCover N).
Apply andI to the current goal.
Let u be given.
Assume Hu: u ∈ BallCover N.
We will prove u ∈ Tx.
Apply (ReplE_impred X (λx0 : set ⇒ open_ball X d x0 (eps_ N)) u Hu) to the current goal.
Let x0 be given.
Assume Hx0X: x0 ∈ X.
Assume HuEq: u = open_ball X d x0 (eps_ N).
rewrite the current goal using HuEq (from left to right).
We prove the intermediate claim HuIn: open_ball X d x0 (eps_ N) ∈ metric_topology X d.
An exact proof term for the current goal is (open_ball_in_metric_topology X d x0 (eps_ N) Hm Hx0X HepsPos).
rewrite the current goal using HTdef (from right to left).
An exact proof term for the current goal is HuIn.
Let x0 be given.
Assume Hx0X: x0 ∈ X.
We will prove ∃u : set, u ∈ BallCover N ∧ x0 ∈ u.
We use (open_ball X d x0 (eps_ N)) to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (ReplI X (λx1 : set ⇒ open_ball X d x1 (eps_ N)) x0 Hx0X).
An exact proof term for the current goal is (center_in_open_ball X d x0 (eps_ N) Hm Hx0X HepsPos).
We prove the intermediate claim HexV: ∃V : set, countable_subcollection V (BallCover N) ∧ covers X V.
An exact proof term for the current goal is (HLprop (BallCover N) Hcover).
An exact proof term for the current goal is (Eps_i_ex (λV : set ⇒ countable_subcollection V (BallCover N) ∧ covers X V) HexV).
Set Pair to be the term ∑n ∈ ω, Vsel n.
Set choose_center to be the term λp : set ⇒ Eps_i (λc : set ⇒ c ∈ X ∧ (p 1) = open_ball X d c (eps_ (p 0))) of type set → set.
Set D0 to be the term {choose_center p|p ∈ Pair}.
We prove the intermediate claim HD0count: countable_set D0.
We prove the intermediate claim HomegaCount: countable_set ω.
We will prove countable_set ω.
We will prove countable ω.
An exact proof term for the current goal is (Subq_atleastp ω ω (Subq_ref ω)).
We prove the intermediate claim HPairCount: countable_set Pair.
Set Y to be the term λn : set ⇒ Vsel n of type set → set.
We prove the intermediate claim HY: ∀n : set, n ∈ ω → countable (Y n).
Let n be given.
Assume Hn: n ∈ ω.
We prove the intermediate claim Hspec: countable_subcollection (Vsel n) (BallCover n) ∧ covers X (Vsel n).
An exact proof term for the current goal is (HVsel_spec n Hn).
We prove the intermediate claim Hsubcount: countable_subcollection (Vsel n) (BallCover n).
An exact proof term for the current goal is (andEL (countable_subcollection (Vsel n) (BallCover n)) (covers X (Vsel n)) Hspec).
An exact proof term for the current goal is (andER ((Vsel n) ⊆ BallCover n) (countable_set (Vsel n)) Hsubcount).
An exact proof term for the current goal is (Sigma_countable ω HomegaCount Y HY).
An exact proof term for the current goal is (countable_image Pair HPairCount choose_center).
We prove the intermediate claim HD0subX: D0 ⊆ X.
Let c be given.
Assume Hc: c ∈ D0.
Apply (ReplE_impred Pair choose_center c Hc) to the current goal.
Let p be given.
Assume Hp: p ∈ Pair.
Assume Hceq: c = choose_center p.
We prove the intermediate claim HnOmega: (p 0) ∈ ω.
An exact proof term for the current goal is (ap0_Sigma ω (λn : set ⇒ Vsel n) p Hp).
We prove the intermediate claim HbIn: (p 1) ∈ Vsel (p 0).
An exact proof term for the current goal is (ap1_Sigma ω (λn : set ⇒ Vsel n) p Hp).
We prove the intermediate claim Hspec: countable_subcollection (Vsel (p 0)) (BallCover (p 0)) ∧ covers X (Vsel (p 0)).
An exact proof term for the current goal is (HVsel_spec (p 0) HnOmega).
We prove the intermediate claim HVsub: (Vsel (p 0)) ⊆ BallCover (p 0).
An exact proof term for the current goal is (andEL ((Vsel (p 0)) ⊆ BallCover (p 0)) (countable_set (Vsel (p 0))) (andEL (countable_subcollection (Vsel (p 0)) (BallCover (p 0))) (covers X (Vsel (p 0))) Hspec)).
We prove the intermediate claim HbCover: (p 1) ∈ BallCover (p 0).
An exact proof term for the current goal is (HVsub (p 1) HbIn).
We prove the intermediate claim HexC: ∃x0 ∈ X, (p 1) = open_ball X d x0 (eps_ (p 0)).
Apply (ReplE X (λx0 : set ⇒ open_ball X d x0 (eps_ (p 0))) (p 1) HbCover) to the current goal.
Apply HexC to the current goal.
Let x0 be given.
Assume Hx0pair.
We prove the intermediate claim Hx0X: x0 ∈ X.
An exact proof term for the current goal is (andEL (x0 ∈ X) ((p 1) = open_ball X d x0 (eps_ (p 0))) Hx0pair).
We prove the intermediate claim HbEq: (p 1) = open_ball X d x0 (eps_ (p 0)).
An exact proof term for the current goal is (andER (x0 ∈ X) ((p 1) = open_ball X d x0 (eps_ (p 0))) Hx0pair).
We prove the intermediate claim HchooseSpec: choose_center p ∈ X ∧ (p 1) = open_ball X d (choose_center p) (eps_ (p 0)).
We prove the intermediate claim HexC2: ∃c0 : set, c0 ∈ X ∧ (p 1) = open_ball X d c0 (eps_ (p 0)).
We use x0 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hx0X.
An exact proof term for the current goal is HbEq.
An exact proof term for the current goal is (Eps_i_ex (λc0 : set ⇒ c0 ∈ X ∧ (p 1) = open_ball X d c0 (eps_ (p 0))) HexC2).
rewrite the current goal using Hceq (from left to right).
An exact proof term for the current goal is (andEL (choose_center p ∈ X) ((p 1) = open_ball X d (choose_center p) (eps_ (p 0))) HchooseSpec).
We prove the intermediate claim HD0dense: dense_in D0 X Tx.
We will prove closure_of X Tx D0 = X.
Apply set_ext to the current goal.
An exact proof term for the current goal is (closure_in_space X Tx D0 HLtop).
Let x be given.
Assume HxX: x ∈ X.
We will prove x ∈ closure_of X Tx D0.
We prove the intermediate claim Hcliff: x ∈ closure_of X Tx D0 ↔ (∀U ∈ Tx, x ∈ U → U ∩ D0 ≠ Empty).
An exact proof term for the current goal is (closure_characterization X Tx D0 x HLtop HxX).
We prove the intermediate claim Hneigh: ∀U ∈ Tx, x ∈ U → U ∩ D0 ≠ Empty.
Let U be given.
Assume HU: U ∈ Tx.
Assume HxU: x ∈ U.
We prove the intermediate claim HexBall: ∃r ∈ R, Rlt 0 r ∧ open_ball X d x r ⊆ U.
Set B0 to be the term famunion X (λc : set ⇒ {open_ball X d c r|r ∈ R, Rlt 0 r}).
We prove the intermediate claim Hdef: metric_topology X d = generated_topology X B0.
Use reflexivity.
We prove the intermediate claim HUgen: U ∈ generated_topology X B0.
We will prove U ∈ generated_topology X B0.
rewrite the current goal using Hdef (from right to left).
rewrite the current goal using HTdef (from left to right).
An exact proof term for the current goal is HU.
We prove the intermediate claim HUcond: ∀y ∈ U, ∃b0 ∈ B0, y ∈ b0 ∧ b0 ⊆ U.
An exact proof term for the current goal is (SepE2 (𝒫 X) (λU0 : set ⇒ ∀y : set, y ∈ U0 → ∃b0 ∈ B0, y ∈ b0 ∧ b0 ⊆ U0) U HUgen).
We prove the intermediate claim Hexb0: ∃b0 ∈ B0, x ∈ b0 ∧ b0 ⊆ U.
An exact proof term for the current goal is (HUcond x HxU).
Apply Hexb0 to the current goal.
Let b0 be given.
Assume Hb0pair.
We prove the intermediate claim Hb0B0: b0 ∈ B0.
An exact proof term for the current goal is (andEL (b0 ∈ B0) (x ∈ b0 ∧ b0 ⊆ U) Hb0pair).
We prove the intermediate claim Hxinb0: x ∈ b0.
An exact proof term for the current goal is (andEL (x ∈ b0) (b0 ⊆ U) (andER (b0 ∈ B0) (x ∈ b0 ∧ b0 ⊆ U) Hb0pair)).
We prove the intermediate claim Hb0sub: b0 ⊆ U.
An exact proof term for the current goal is (andER (x ∈ b0) (b0 ⊆ U) (andER (b0 ∈ B0) (x ∈ b0 ∧ b0 ⊆ U) Hb0pair)).
Apply (famunionE_impred X (λc : set ⇒ {open_ball X d c r|r ∈ R, Rlt 0 r}) b0 Hb0B0 (∃r ∈ R, Rlt 0 r ∧ open_ball X d x r ⊆ U)) to the current goal.
Let c be given.
Assume HcX: c ∈ X.
Assume Hb0In: b0 ∈ {open_ball X d c r|r ∈ R, Rlt 0 r}.
Apply (ReplSepE_impred R (λr0 : set ⇒ Rlt 0 r0) (λr0 : set ⇒ open_ball X d c r0) b0 Hb0In (∃r ∈ R, Rlt 0 r ∧ open_ball X d x r ⊆ U)) to the current goal.
Let r0 be given.
Assume Hr0R: r0 ∈ R.
Assume Hr0pos: Rlt 0 r0.
Assume Hb0eq: b0 = open_ball X d c r0.
We prove the intermediate claim HxinBall: x ∈ open_ball X d c r0.
rewrite the current goal using Hb0eq (from right to left).
An exact proof term for the current goal is Hxinb0.
We prove the intermediate claim HballsubU: open_ball X d c r0 ⊆ U.
We will prove open_ball X d c r0 ⊆ U.
rewrite the current goal using Hb0eq (from right to left).
An exact proof term for the current goal is Hb0sub.
We prove the intermediate claim Hexs: ∃s : set, s ∈ R ∧ Rlt 0 s ∧ open_ball X d x s ⊆ open_ball X d c r0.
An exact proof term for the current goal is (open_ball_refine_center X d c x r0 Hm HcX HxX Hr0R Hr0pos HxinBall).
Apply Hexs to the current goal.
Let s be given.
Assume Hs.
We prove the intermediate claim HsRpos: s ∈ R ∧ Rlt 0 s.
An exact proof term for the current goal is (andEL (s ∈ R ∧ Rlt 0 s) (open_ball X d x s ⊆ open_ball X d c r0) Hs).
We prove the intermediate claim HsR: s ∈ R.
An exact proof term for the current goal is (andEL (s ∈ R) (Rlt 0 s) HsRpos).
We prove the intermediate claim Hspos: Rlt 0 s.
An exact proof term for the current goal is (andER (s ∈ R) (Rlt 0 s) HsRpos).
We prove the intermediate claim HsubBall: open_ball X d x s ⊆ open_ball X d c r0.
An exact proof term for the current goal is (andER (s ∈ R ∧ Rlt 0 s) (open_ball X d x s ⊆ open_ball X d c r0) Hs).
We prove the intermediate claim HsubU: open_ball X d x s ⊆ U.
An exact proof term for the current goal is (Subq_tra (open_ball X d x s) (open_ball X d c r0) U HsubBall HballsubU).
We use s to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HsR.
Apply andI to the current goal.
An exact proof term for the current goal is Hspos.
An exact proof term for the current goal is HsubU.
Apply HexBall to the current goal.
Let r be given.
Assume Hrpack.
We prove the intermediate claim HrR: r ∈ R.
An exact proof term for the current goal is (andEL (r ∈ R) (Rlt 0 r ∧ open_ball X d x r ⊆ U) Hrpack).
We prove the intermediate claim Hrprop: Rlt 0 r ∧ open_ball X d x r ⊆ U.
An exact proof term for the current goal is (andER (r ∈ R) (Rlt 0 r ∧ open_ball X d x r ⊆ U) Hrpack).
We prove the intermediate claim Hrpos: Rlt 0 r.
An exact proof term for the current goal is (andEL (Rlt 0 r) (open_ball X d x r ⊆ U) Hrprop).
We prove the intermediate claim Hballsub: open_ball X d x r ⊆ U.
An exact proof term for the current goal is (andER (Rlt 0 r) (open_ball X d x r ⊆ U) Hrprop).
We prove the intermediate claim HexN: ∃N ∈ ω, eps_ N < r.
An exact proof term for the current goal is (exists_eps_lt_pos r HrR Hrpos).
Apply HexN to the current goal.
Let N be given.
Assume HNpair.
We prove the intermediate claim HNomega: N ∈ ω.
An exact proof term for the current goal is (andEL (N ∈ ω) (eps_ N < r) HNpair).
We prove the intermediate claim HepsLt: eps_ N < r.
An exact proof term for the current goal is (andER (N ∈ ω) (eps_ N < r) HNpair).
We prove the intermediate claim HepsR: eps_ N ∈ R.
An exact proof term for the current goal is (SNoS_omega_real (eps_ N) (SNo_eps_SNoS_omega N HNomega)).
We prove the intermediate claim HepsRlt: Rlt (eps_ N) r.
An exact proof term for the current goal is (RltI (eps_ N) r HepsR HrR HepsLt).
We prove the intermediate claim Hspec: countable_subcollection (Vsel N) (BallCover N) ∧ covers X (Vsel N).
An exact proof term for the current goal is (HVsel_spec N HNomega).
We prove the intermediate claim Hcov: covers X (Vsel N).
An exact proof term for the current goal is (andER (countable_subcollection (Vsel N) (BallCover N)) (covers X (Vsel N)) Hspec).
We prove the intermediate claim Hexb: ∃b : set, b ∈ Vsel N ∧ x ∈ b.
An exact proof term for the current goal is (Hcov x HxX).
Apply Hexb to the current goal.
Let b be given.
Assume Hbpair.
We prove the intermediate claim HbIn: b ∈ Vsel N.
An exact proof term for the current goal is (andEL (b ∈ Vsel N) (x ∈ b) Hbpair).
We prove the intermediate claim Hxb: x ∈ b.
An exact proof term for the current goal is (andER (b ∈ Vsel N) (x ∈ b) Hbpair).
We prove the intermediate claim Hsubcov: (Vsel N) ⊆ BallCover N.
An exact proof term for the current goal is (andEL ((Vsel N) ⊆ BallCover N) (countable_set (Vsel N)) (andEL (countable_subcollection (Vsel N) (BallCover N)) (covers X (Vsel N)) Hspec)).
We prove the intermediate claim HbCover: b ∈ BallCover N.
An exact proof term for the current goal is (Hsubcov b HbIn).
We prove the intermediate claim HexC: ∃c0 ∈ X, b = open_ball X d c0 (eps_ N).
Apply (ReplE X (λx0 : set ⇒ open_ball X d x0 (eps_ N)) b HbCover) to the current goal.
Apply HexC to the current goal.
Let c0 be given.
Assume Hc0pair.
We prove the intermediate claim Hc0X: c0 ∈ X.
An exact proof term for the current goal is (andEL (c0 ∈ X) (b = open_ball X d c0 (eps_ N)) Hc0pair).
We prove the intermediate claim HbEq: b = open_ball X d c0 (eps_ N).
An exact proof term for the current goal is (andER (c0 ∈ X) (b = open_ball X d c0 (eps_ N)) Hc0pair).
We prove the intermediate claim HpSig: (N,b) ∈ Pair.
An exact proof term for the current goal is (tuple_2_Sigma ω (λn0 : set ⇒ Vsel n0) N HNomega b HbIn).
Set c to be the term choose_center (N,b).
We prove the intermediate claim HcInD0: c ∈ D0.
An exact proof term for the current goal is (ReplI Pair choose_center (N,b) HpSig).
We prove the intermediate claim HchooseRaw: c ∈ X ∧ ((N,b) 1) = open_ball X d c (eps_ ((N,b) 0)).
We prove the intermediate claim HexC2: ∃c1 : set, c1 ∈ X ∧ ((N,b) 1) = open_ball X d c1 (eps_ ((N,b) 0)).
We use c0 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hc0X.
rewrite the current goal using (tuple_2_1_eq N b) (from left to right).
rewrite the current goal using (tuple_2_0_eq N b) (from left to right).
An exact proof term for the current goal is HbEq.
An exact proof term for the current goal is (Eps_i_ex (λc1 : set ⇒ c1 ∈ X ∧ ((N,b) 1) = open_ball X d c1 (eps_ ((N,b) 0))) HexC2).
We prove the intermediate claim HcX: c ∈ X.
An exact proof term for the current goal is (andEL (c ∈ X) (((N,b) 1) = open_ball X d c (eps_ ((N,b) 0))) HchooseRaw).
We prove the intermediate claim HxInBall: x ∈ open_ball X d c (eps_ N).
We will prove x ∈ open_ball X d c (eps_ N).
We prove the intermediate claim Htmp: ((N,b) 1) = open_ball X d c (eps_ ((N,b) 0)).
An exact proof term for the current goal is (andER (c ∈ X) (((N,b) 1) = open_ball X d c (eps_ ((N,b) 0))) HchooseRaw).
We prove the intermediate claim HxInb1: x ∈ ((N,b) 1).
We will prove x ∈ ((N,b) 1).
rewrite the current goal using (tuple_2_1_eq N b) (from left to right).
An exact proof term for the current goal is Hxb.
We prove the intermediate claim HxInBall0: x ∈ open_ball X d c (eps_ ((N,b) 0)).
We will prove x ∈ open_ball X d c (eps_ ((N,b) 0)).
rewrite the current goal using Htmp (from right to left).
An exact proof term for the current goal is HxInb1.
We prove the intermediate claim HepsEq: eps_ ((N,b) 0) = eps_ N.
rewrite the current goal using (tuple_2_0_eq N b) (from left to right).
Use reflexivity.
rewrite the current goal using HepsEq (from right to left).
An exact proof term for the current goal is HxInBall0.
We prove the intermediate claim Hdxc: Rlt (apply_fun d (c,x)) (eps_ N).
An exact proof term for the current goal is (open_ballE2 X d c (eps_ N) x HxInBall).
We prove the intermediate claim Hsym: apply_fun d (x,c) = apply_fun d (c,x).
An exact proof term for the current goal is (metric_on_symmetric X d x c Hm HxX HcX).
We prove the intermediate claim Hdxc2: Rlt (apply_fun d (x,c)) (eps_ N).
rewrite the current goal using Hsym (from left to right).
An exact proof term for the current goal is Hdxc.
We prove the intermediate claim Hdxc3: Rlt (apply_fun d (x,c)) r.
An exact proof term for the current goal is (Rlt_tra (apply_fun d (x,c)) (eps_ N) r Hdxc2 HepsRlt).
We prove the intermediate claim HcInBallxr: c ∈ open_ball X d x r.
An exact proof term for the current goal is (open_ballI X d x r c HcX Hdxc3).
We prove the intermediate claim HcInU: c ∈ U.
An exact proof term for the current goal is (Hballsub c HcInBallxr).
We will prove U ∩ D0 ≠ Empty.
We prove the intermediate claim Hwd: c ∈ U ∩ D0.
An exact proof term for the current goal is (binintersectI U D0 c HcInU HcInD0).
An exact proof term for the current goal is (elem_implies_nonempty (U ∩ D0) c Hwd).
An exact proof term for the current goal is (iffER (x ∈ closure_of X Tx D0) (∀U ∈ Tx, x ∈ U → U ∩ D0 ≠ Empty) Hcliff Hneigh).
Apply (ex30_5a_metrizable_countable_dense_second_countable X Tx) to the current goal.
An exact proof term for the current goal is Hmet.
We use D0 to witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HD0subX.
An exact proof term for the current goal is HD0count.
An exact proof term for the current goal is HD0dense.
∎