Let X, Tx and d be given.
Assume Hcomp: compact_space X Tx.
Assume Hmet: metrizable X Tx.
Assume Hd: metric_on X d.
Assume HTdef: Tx = metric_topology X d.
We will prove second_countable_space X Tx.
We prove the intermediate claim HL: Lindelof_space X Tx.
We will prove topology_on X Tx ∧ ∀U : set, open_cover X Tx U → ∃V : set, countable_subcollection V U ∧ covers X V.
Apply andI to the current goal.
An exact proof term for the current goal is (compact_space_topology X Tx Hcomp).
Let U be given.
Assume Hcover: open_cover X Tx U.
We will prove ∃V : set, countable_subcollection V U ∧ covers X V.
We prove the intermediate claim HTx: topology_on X Tx.
An exact proof term for the current goal is (compact_space_topology X Tx Hcomp).
We prove the intermediate claim HUpow: U ⊆ 𝒫 X.
An exact proof term for the current goal is (open_cover_family_sub X Tx U HTx Hcover).
We prove the intermediate claim HcovOf: open_cover_of X Tx U.
We will prove topology_on X Tx ∧ U ⊆ 𝒫 X ∧ X ⊆ ⋃ U ∧ (∀W : set, W ∈ U → W ∈ Tx).
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HTx.
An exact proof term for the current goal is HUpow.
Let x be given.
Assume HxX: x ∈ X.
We will prove x ∈ ⋃ U.
We prove the intermediate claim Hcov: covers X U.
An exact proof term for the current goal is (andER (∀u0 : set, u0 ∈ U → u0 ∈ Tx) (covers X U) Hcover).
We prove the intermediate claim Hexu: ∃u : set, u ∈ U ∧ x ∈ u.
An exact proof term for the current goal is (Hcov x HxX).
Apply Hexu to the current goal.
Let u be given.
Assume Hupair: u ∈ U ∧ x ∈ u.
An exact proof term for the current goal is (UnionI U x u (andER (u ∈ U) (x ∈ u) Hupair) (andEL (u ∈ U) (x ∈ u) Hupair)).
An exact proof term for the current goal is (andEL (∀u0 : set, u0 ∈ U → u0 ∈ Tx) (covers X U) Hcover).
We prove the intermediate claim Hfin: has_finite_subcover X Tx U.
An exact proof term for the current goal is (compact_space_subcover_property X Tx Hcomp U HcovOf).
Apply Hfin to the current goal.
Let G be given.
Assume HG: G ⊆ U ∧ finite G ∧ X ⊆ ⋃ G.
We use G to witness the existential quantifier.
We will prove countable_subcollection G U ∧ covers X G.
Apply andI to the current goal.
We will prove G ⊆ U ∧ countable_set G.
Apply andI to the current goal.
We prove the intermediate claim HGleft: G ⊆ U ∧ finite G.
An exact proof term for the current goal is (andEL (G ⊆ U ∧ finite G) (X ⊆ ⋃ G) HG).
An exact proof term for the current goal is (andEL (G ⊆ U) (finite G) HGleft).
We prove the intermediate claim HGleft: G ⊆ U ∧ finite G.
An exact proof term for the current goal is (andEL (G ⊆ U ∧ finite G) (X ⊆ ⋃ G) HG).
We prove the intermediate claim HGfin: finite G.
An exact proof term for the current goal is (andER (G ⊆ U) (finite G) HGleft).
An exact proof term for the current goal is (finite_countable G HGfin).
Let x be given.
Assume HxX: x ∈ X.
We will prove ∃u : set, u ∈ G ∧ x ∈ u.
We prove the intermediate claim HXsub: X ⊆ ⋃ G.
An exact proof term for the current goal is (andER (G ⊆ U ∧ finite G) (X ⊆ ⋃ G) HG).
We prove the intermediate claim HxUnion: x ∈ ⋃ G.
An exact proof term for the current goal is (HXsub x HxX).
Apply (UnionE G x HxUnion) to the current goal.
Let u be given.
Assume Hux: x ∈ u ∧ u ∈ G.
We use u to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (andER (x ∈ u) (u ∈ G) Hux).
An exact proof term for the current goal is (andEL (x ∈ u) (u ∈ G) Hux).
We will prove topology_on X Tx ∧ ∃B : set, basis_on X B ∧ countable_set B ∧ basis_generates X B Tx.
Apply andI to the current goal.
An exact proof term for the current goal is (compact_space_topology X Tx Hcomp).
We prove the intermediate claim HTx: topology_on X Tx.
An exact proof term for the current goal is (compact_space_topology X Tx Hcomp).
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 ⇒ V ⊆ BallCover N ∧ finite V ∧ X ⊆ ⋃ V) of type set → set.
We prove the intermediate claim HVsel_spec: ∀N : set, N ∈ ω → Vsel N ⊆ BallCover N ∧ finite (Vsel N) ∧ X ⊆ ⋃ (Vsel N).
Let N be given.
Assume HNomega: N ∈ ω.
We will prove Vsel N ⊆ BallCover N ∧ finite (Vsel N) ∧ 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 HcovOf: open_cover_of X Tx (BallCover N).
We will prove topology_on X Tx ∧ BallCover N ⊆ 𝒫 X ∧ X ⊆ ⋃ (BallCover N) ∧ (∀U : set, U ∈ BallCover N → U ∈ Tx).
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HTx.
Let b be given.
Assume Hb: b ∈ BallCover N.
We will prove b ∈ 𝒫 X.
Apply (ReplE_impred X (λx0 : set ⇒ open_ball X d x0 (eps_ N)) b Hb) to the current goal.
Let x0 be given.
Assume Hx0X: x0 ∈ X.
Assume HbEq: b = open_ball X d x0 (eps_ N).
rewrite the current goal using HbEq (from left to right).
Apply PowerI to the current goal.
An exact proof term for the current goal is (open_ball_subset_X X d x0 (eps_ N)).
Let x0 be given.
Assume Hx0X: x0 ∈ X.
We will prove x0 ∈ ⋃ (BallCover N).
Set b0 to be the term open_ball X d x0 (eps_ N).
We prove the intermediate claim Hb0In: b0 ∈ BallCover N.
An exact proof term for the current goal is (ReplI X (λx1 : set ⇒ open_ball X d x1 (eps_ N)) x0 Hx0X).
We prove the intermediate claim Hx0b0: x0 ∈ b0.
An exact proof term for the current goal is (center_in_open_ball X d x0 (eps_ N) Hd Hx0X HepsPos).
An exact proof term for the current goal is (UnionI (BallCover N) x0 b0 Hx0b0 Hb0In).
Let b be given.
Assume Hb: b ∈ BallCover N.
We will prove b ∈ Tx.
Apply (ReplE_impred X (λx0 : set ⇒ open_ball X d x0 (eps_ N)) b Hb) to the current goal.
Let x0 be given.
Assume Hx0X: x0 ∈ X.
Assume HbEq: b = open_ball X d x0 (eps_ N).
rewrite the current goal using HbEq (from left to right).
We prove the intermediate claim HbIn: 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) Hd Hx0X HepsPos).
rewrite the current goal using HTdef (from left to right).
An exact proof term for the current goal is HbIn.
We prove the intermediate claim Hfin: has_finite_subcover X Tx (BallCover N).
An exact proof term for the current goal is (compact_space_subcover_property X Tx Hcomp (BallCover N) HcovOf).
An exact proof term for the current goal is (Eps_i_ex (λV : set ⇒ V ⊆ BallCover N ∧ finite V ∧ X ⊆ ⋃ V) Hfin).
Set Pair to be the term ∑n ∈ ω, Vsel (ordsucc n).
Set B to be the term {p 1|p ∈ Pair}.
We prove the intermediate claim HBcount: countable_set B.
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 (ordsucc 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 Hsucc: ordsucc n ∈ ω.
An exact proof term for the current goal is (omega_ordsucc n Hn).
We prove the intermediate claim Hspec: Vsel (ordsucc n) ⊆ BallCover (ordsucc n) ∧ finite (Vsel (ordsucc n)) ∧ X ⊆ ⋃ (Vsel (ordsucc n)).
An exact proof term for the current goal is (HVsel_spec (ordsucc n) Hsucc).
We prove the intermediate claim Hleft: Vsel (ordsucc n) ⊆ BallCover (ordsucc n) ∧ finite (Vsel (ordsucc n)).
An exact proof term for the current goal is (andEL (Vsel (ordsucc n) ⊆ BallCover (ordsucc n) ∧ finite (Vsel (ordsucc n))) (X ⊆ ⋃ (Vsel (ordsucc n))) Hspec).
We prove the intermediate claim HfinV: finite (Vsel (ordsucc n)).
An exact proof term for the current goal is (andER (Vsel (ordsucc n) ⊆ BallCover (ordsucc n)) (finite (Vsel (ordsucc n))) Hleft).
An exact proof term for the current goal is (finite_countable (Vsel (ordsucc n)) HfinV).
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 (λp : set ⇒ p 1)).
We prove the intermediate claim HBsub: B ⊆ 𝒫 X.
Let b be given.
Assume Hb: b ∈ B.
We will prove b ∈ 𝒫 X.
Apply (ReplE_impred Pair (λp : set ⇒ p 1) b Hb) to the current goal.
Let p be given.
Assume Hp: p ∈ Pair.
Assume HbEq: b = p 1.
We prove the intermediate claim HnOmega: (p 0) ∈ ω.
An exact proof term for the current goal is (ap0_Sigma ω (λn0 : set ⇒ Vsel (ordsucc n0)) p Hp).
We prove the intermediate claim HbInV: (p 1) ∈ Vsel (ordsucc (p 0)).
An exact proof term for the current goal is (ap1_Sigma ω (λn0 : set ⇒ Vsel (ordsucc n0)) p Hp).
We prove the intermediate claim Hsucc: ordsucc (p 0) ∈ ω.
An exact proof term for the current goal is (omega_ordsucc (p 0) HnOmega).
We prove the intermediate claim Hspec: Vsel (ordsucc (p 0)) ⊆ BallCover (ordsucc (p 0)) ∧ finite (Vsel (ordsucc (p 0))) ∧ X ⊆ ⋃ (Vsel (ordsucc (p 0))).
An exact proof term for the current goal is (HVsel_spec (ordsucc (p 0)) Hsucc).
We prove the intermediate claim Hleft: Vsel (ordsucc (p 0)) ⊆ BallCover (ordsucc (p 0)) ∧ finite (Vsel (ordsucc (p 0))).
An exact proof term for the current goal is (andEL (Vsel (ordsucc (p 0)) ⊆ BallCover (ordsucc (p 0)) ∧ finite (Vsel (ordsucc (p 0)))) (X ⊆ ⋃ (Vsel (ordsucc (p 0)))) Hspec).
We prove the intermediate claim HVsub: Vsel (ordsucc (p 0)) ⊆ BallCover (ordsucc (p 0)).
An exact proof term for the current goal is (andEL (Vsel (ordsucc (p 0)) ⊆ BallCover (ordsucc (p 0))) (finite (Vsel (ordsucc (p 0)))) Hleft).
We prove the intermediate claim HbCover: (p 1) ∈ BallCover (ordsucc (p 0)).
An exact proof term for the current goal is (HVsub (p 1) HbInV).
Apply (ReplE X (λx0 : set ⇒ open_ball X d x0 (eps_ (ordsucc (p 0)))) (p 1) HbCover) to the current goal.
Let x0 be given.
Assume Hx0pair: x0 ∈ X ∧ (p 1) = open_ball X d x0 (eps_ (ordsucc (p 0))).
We prove the intermediate claim Hbeq: (p 1) = open_ball X d x0 (eps_ (ordsucc (p 0))).
An exact proof term for the current goal is (andER (x0 ∈ X) ((p 1) = open_ball X d x0 (eps_ (ordsucc (p 0)))) Hx0pair).
rewrite the current goal using HbEq (from left to right).
rewrite the current goal using Hbeq (from left to right).
Apply PowerI to the current goal.
An exact proof term for the current goal is (open_ball_subset_X X d x0 (eps_ (ordsucc (p 0)))).
We prove the intermediate claim HBrefines: basis_refines X B Tx.
We will prove topology_on X Tx ∧ (∀U ∈ Tx, ∀x ∈ U, ∃b ∈ B, x ∈ b ∧ b ⊆ U).
Apply andI to the current goal.
An exact proof term for the current goal is HTx.
Let U be given.
Assume HU: U ∈ Tx.
We will prove ∀x : set, x ∈ U → ∃b ∈ B, x ∈ b ∧ b ⊆ U.
Let x be given.
Assume HxU: x ∈ U.
We will prove ∃b ∈ B, x ∈ b ∧ b ⊆ U.
We prove the intermediate claim HUPow: U ∈ 𝒫 X.
An exact proof term for the current goal is (topology_subset_axiom X Tx HTx U HU).
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is ((PowerE X U HUPow) x HxU).
We prove the intermediate claim HUmt: U ∈ metric_topology X d.
rewrite the current goal using HTdef (from right to left).
An exact proof term for the current goal is HU.
We prove the intermediate claim HexBall: ∃r : set, r ∈ R ∧ (Rlt 0 r ∧ open_ball X d x r ⊆ U).
An exact proof term for the current goal is (metric_topology_neighborhood_contains_ball X d x U Hd HxX HUmt HxU).
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).
Set s to be the term eps_ (ordsucc N).
We prove the intermediate claim HsDef: s = eps_ (ordsucc N).
Use reflexivity.
We prove the intermediate claim HsuccOmega: ordsucc N ∈ ω.
An exact proof term for the current goal is (omega_ordsucc N HNomega).
We prove the intermediate claim HsR: s ∈ R.
rewrite the current goal using HsDef (from left to right).
An exact proof term for the current goal is (SNoS_omega_real (eps_ (ordsucc N)) (SNo_eps_SNoS_omega (ordsucc N) HsuccOmega)).
We prove the intermediate claim HsposS: 0 < s.
rewrite the current goal using HsDef (from left to right).
An exact proof term for the current goal is (SNo_eps_pos (ordsucc N) HsuccOmega).
We prove the intermediate claim Hspos: Rlt 0 s.
An exact proof term for the current goal is (RltI 0 s real_0 HsR HsposS).
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 HsSumLt: Rlt (add_SNo s s) r.
We prove the intermediate claim HNnat: nat_p N.
An exact proof term for the current goal is (omega_nat_p N HNomega).
We prove the intermediate claim HsumEq: add_SNo s s = eps_ N.
rewrite the current goal using HsDef (from left to right).
rewrite the current goal using HsDef (from left to right) at position 2.
An exact proof term for the current goal is (eps_ordsucc_half_add N HNnat).
rewrite the current goal using HsumEq (from left to right).
An exact proof term for the current goal is HepsRlt.
We prove the intermediate claim Hspec: Vsel (ordsucc N) ⊆ BallCover (ordsucc N) ∧ finite (Vsel (ordsucc N)) ∧ X ⊆ ⋃ (Vsel (ordsucc N)).
An exact proof term for the current goal is (HVsel_spec (ordsucc N) HsuccOmega).
We prove the intermediate claim HXsub: X ⊆ ⋃ (Vsel (ordsucc N)).
An exact proof term for the current goal is (andER (Vsel (ordsucc N) ⊆ BallCover (ordsucc N) ∧ finite (Vsel (ordsucc N))) (X ⊆ ⋃ (Vsel (ordsucc N))) Hspec).
We prove the intermediate claim HxUnion: x ∈ ⋃ (Vsel (ordsucc N)).
An exact proof term for the current goal is (HXsub x HxX).
Apply (UnionE (Vsel (ordsucc N)) x HxUnion) to the current goal.
Let b be given.
Assume Hbx: x ∈ b ∧ b ∈ Vsel (ordsucc N).
We use b to witness the existential quantifier.
We will prove b ∈ B ∧ (x ∈ b ∧ b ⊆ U).
Apply andI to the current goal.
We prove the intermediate claim HbInV: b ∈ Vsel (ordsucc N).
An exact proof term for the current goal is (andER (x ∈ b) (b ∈ Vsel (ordsucc N)) Hbx).
We prove the intermediate claim HpSig: (N,b) ∈ Pair.
An exact proof term for the current goal is (tuple_2_Sigma ω (λn0 : set ⇒ Vsel (ordsucc n0)) N HNomega b HbInV).
We prove the intermediate claim HbEq1: (N,b) 1 = b.
An exact proof term for the current goal is (tuple_2_1_eq N b).
rewrite the current goal using HbEq1 (from right to left) at position 1.
An exact proof term for the current goal is (ReplI Pair (λp : set ⇒ p 1) (N,b) HpSig).
Apply andI to the current goal.
An exact proof term for the current goal is (andEL (x ∈ b) (b ∈ Vsel (ordsucc N)) Hbx).
We prove the intermediate claim Hleft: Vsel (ordsucc N) ⊆ BallCover (ordsucc N) ∧ finite (Vsel (ordsucc N)).
An exact proof term for the current goal is (andEL (Vsel (ordsucc N) ⊆ BallCover (ordsucc N) ∧ finite (Vsel (ordsucc N))) (X ⊆ ⋃ (Vsel (ordsucc N))) Hspec).
We prove the intermediate claim HVsub: Vsel (ordsucc N) ⊆ BallCover (ordsucc N).
An exact proof term for the current goal is (andEL (Vsel (ordsucc N) ⊆ BallCover (ordsucc N)) (finite (Vsel (ordsucc N))) Hleft).
We prove the intermediate claim HbCover: b ∈ BallCover (ordsucc N).
An exact proof term for the current goal is (HVsub b (andER (x ∈ b) (b ∈ Vsel (ordsucc N)) Hbx)).
Apply (ReplE X (λc0 : set ⇒ open_ball X d c0 (eps_ (ordsucc N))) b HbCover) to the current goal.
Let c0 be given.
Assume Hc0pair: c0 ∈ X ∧ b = open_ball X d c0 (eps_ (ordsucc N)).
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_ (ordsucc N))) Hc0pair).
We prove the intermediate claim HbDef: b = open_ball X d c0 (eps_ (ordsucc N)).
An exact proof term for the current goal is (andER (c0 ∈ X) (b = open_ball X d c0 (eps_ (ordsucc N))) Hc0pair).
We prove the intermediate claim HsubBall: b ⊆ open_ball X d x r.
Let y be given.
Assume Hy: y ∈ b.
We will prove y ∈ open_ball X d x r.
We prove the intermediate claim HyBall: y ∈ open_ball X d c0 (eps_ (ordsucc N)).
rewrite the current goal using HbDef (from right to left).
An exact proof term for the current goal is Hy.
We prove the intermediate claim HyX: y ∈ X.
An exact proof term for the current goal is (open_ballE1 X d c0 (eps_ (ordsucc N)) y HyBall).
We prove the intermediate claim Hdy: Rlt (apply_fun d (c0,y)) (eps_ (ordsucc N)).
An exact proof term for the current goal is (open_ballE2 X d c0 (eps_ (ordsucc N)) y HyBall).
We prove the intermediate claim Hxinb: x ∈ open_ball X d c0 (eps_ (ordsucc N)).
rewrite the current goal using HbDef (from right to left).
An exact proof term for the current goal is (andEL (x ∈ b) (b ∈ Vsel (ordsucc N)) Hbx).
We prove the intermediate claim Hdx0: Rlt (apply_fun d (c0,x)) (eps_ (ordsucc N)).
An exact proof term for the current goal is (open_ballE2 X d c0 (eps_ (ordsucc N)) x Hxinb).
We prove the intermediate claim Hsymxc: apply_fun d (x,c0) = apply_fun d (c0,x).
An exact proof term for the current goal is (metric_on_symmetric X d x c0 Hd HxX Hc0X).
We prove the intermediate claim Hdx: Rlt (apply_fun d (x,c0)) (eps_ (ordsucc N)).
rewrite the current goal using Hsymxc (from left to right).
An exact proof term for the current goal is Hdx0.
Set dx to be the term apply_fun d (x,c0).
Set dy to be the term apply_fun d (c0,y).
We prove the intermediate claim HdFun: function_on d (setprod X X) R.
An exact proof term for the current goal is (metric_on_function_on X d Hd).
We prove the intermediate claim HdxR: dx ∈ R.
An exact proof term for the current goal is (HdFun (x,c0) (tuple_2_setprod_by_pair_Sigma X X x c0 HxX Hc0X)).
We prove the intermediate claim HdyR: dy ∈ R.
An exact proof term for the current goal is (HdFun (c0,y) (tuple_2_setprod_by_pair_Sigma X X c0 y Hc0X HyX)).
We prove the intermediate claim HdxS: SNo dx.
An exact proof term for the current goal is (real_SNo dx HdxR).
We prove the intermediate claim HdyS: SNo dy.
An exact proof term for the current goal is (real_SNo dy HdyR).
We prove the intermediate claim HsS: SNo s.
An exact proof term for the current goal is (real_SNo s HsR).
We prove the intermediate claim HdxLtS: dx < s.
rewrite the current goal using HsDef (from left to right).
An exact proof term for the current goal is (RltE_lt dx (eps_ (ordsucc N)) Hdx).
We prove the intermediate claim HdyLtS: dy < s.
rewrite the current goal using HsDef (from left to right).
An exact proof term for the current goal is (RltE_lt dy (eps_ (ordsucc N)) Hdy).
We prove the intermediate claim HsumLt: add_SNo dx dy < add_SNo s s.
An exact proof term for the current goal is (add_SNo_Lt3 dx dy s s HdxS HdyS HsS HsS HdxLtS HdyLtS).
We prove the intermediate claim HsumR: add_SNo dx dy ∈ R.
An exact proof term for the current goal is (real_add_SNo dx HdxR dy HdyR).
We prove the intermediate claim HsumRltR: Rlt (add_SNo dx dy) r.
We prove the intermediate claim HssumR: add_SNo s s ∈ R.
An exact proof term for the current goal is (real_add_SNo s HsR s HsR).
We prove the intermediate claim HsumRlt_ss: Rlt (add_SNo dx dy) (add_SNo s s).
An exact proof term for the current goal is (RltI (add_SNo dx dy) (add_SNo s s) HsumR HssumR HsumLt).
An exact proof term for the current goal is (Rlt_tra (add_SNo dx dy) (add_SNo s s) r HsumRlt_ss HsSumLt).
We prove the intermediate claim Htri: Rle (apply_fun d (x,y)) (add_SNo dx dy).
We prove the intermediate claim Htri0: Rle (apply_fun d (x,y)) (add_SNo (apply_fun d (x,c0)) (apply_fun d (c0,y))).
An exact proof term for the current goal is (metric_triangle_Rle X d x c0 y Hd HxX Hc0X HyX).
Set tmp2 to be the term add_SNo (apply_fun d (x,c0)) (apply_fun d (c0,y)).
We prove the intermediate claim Htmp2Def: tmp2 = add_SNo dx dy.
Use reflexivity.
rewrite the current goal using Htmp2Def (from left to right).
An exact proof term for the current goal is Htri0.
We prove the intermediate claim HdistRlt: Rlt (apply_fun d (x,y)) r.
An exact proof term for the current goal is (Rle_Rlt_tra (apply_fun d (x,y)) (add_SNo dx dy) r Htri HsumRltR).
An exact proof term for the current goal is (open_ballI X d x r y HyX HdistRlt).
An exact proof term for the current goal is (Subq_tra b (open_ball X d x r) U HsubBall Hballsub).
We prove the intermediate claim HBref: ∀U ∈ Tx, ∀x ∈ U, ∃b ∈ B, x ∈ b ∧ b ⊆ U.
An exact proof term for the current goal is (andER (topology_on X Tx) (∀U ∈ Tx, ∀x ∈ U, ∃b ∈ B, x ∈ b ∧ b ⊆ U) HBrefines).
We prove the intermediate claim HBopen: ∀b ∈ B, b ∈ Tx.
Let b be given.
Assume Hb: b ∈ B.
We will prove b ∈ Tx.
Apply (ReplE_impred Pair (λp : set ⇒ p 1) b Hb) to the current goal.
Let p be given.
Assume Hp: p ∈ Pair.
Assume HbEq: b = p 1.
We prove the intermediate claim HnOmega: (p 0) ∈ ω.
An exact proof term for the current goal is (ap0_Sigma ω (λn0 : set ⇒ Vsel (ordsucc n0)) p Hp).
We prove the intermediate claim HbInV: (p 1) ∈ Vsel (ordsucc (p 0)).
An exact proof term for the current goal is (ap1_Sigma ω (λn0 : set ⇒ Vsel (ordsucc n0)) p Hp).
We prove the intermediate claim Hsucc: ordsucc (p 0) ∈ ω.
An exact proof term for the current goal is (omega_ordsucc (p 0) HnOmega).
We prove the intermediate claim Hspec: Vsel (ordsucc (p 0)) ⊆ BallCover (ordsucc (p 0)) ∧ finite (Vsel (ordsucc (p 0))) ∧ X ⊆ ⋃ (Vsel (ordsucc (p 0))).
An exact proof term for the current goal is (HVsel_spec (ordsucc (p 0)) Hsucc).
We prove the intermediate claim Hleft: Vsel (ordsucc (p 0)) ⊆ BallCover (ordsucc (p 0)) ∧ finite (Vsel (ordsucc (p 0))).
An exact proof term for the current goal is (andEL (Vsel (ordsucc (p 0)) ⊆ BallCover (ordsucc (p 0)) ∧ finite (Vsel (ordsucc (p 0)))) (X ⊆ ⋃ (Vsel (ordsucc (p 0)))) Hspec).
We prove the intermediate claim HVsub: Vsel (ordsucc (p 0)) ⊆ BallCover (ordsucc (p 0)).
An exact proof term for the current goal is (andEL (Vsel (ordsucc (p 0)) ⊆ BallCover (ordsucc (p 0))) (finite (Vsel (ordsucc (p 0)))) Hleft).
We prove the intermediate claim HbCover: (p 1) ∈ BallCover (ordsucc (p 0)).
An exact proof term for the current goal is (HVsub (p 1) HbInV).
Apply (ReplE X (λx0 : set ⇒ open_ball X d x0 (eps_ (ordsucc (p 0)))) (p 1) HbCover) to the current goal.
Let x0 be given.
Assume Hx0pair: x0 ∈ X ∧ (p 1) = open_ball X d x0 (eps_ (ordsucc (p 0))).
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_ (ordsucc (p 0)))) Hx0pair).
We prove the intermediate claim HbBall: (p 1) = open_ball X d x0 (eps_ (ordsucc (p 0))).
An exact proof term for the current goal is (andER (x0 ∈ X) ((p 1) = open_ball X d x0 (eps_ (ordsucc (p 0)))) Hx0pair).
We prove the intermediate claim HepsR: eps_ (ordsucc (p 0)) ∈ R.
An exact proof term for the current goal is (SNoS_omega_real (eps_ (ordsucc (p 0))) (SNo_eps_SNoS_omega (ordsucc (p 0)) Hsucc)).
We prove the intermediate claim HepsPosS: 0 < eps_ (ordsucc (p 0)).
An exact proof term for the current goal is (SNo_eps_pos (ordsucc (p 0)) Hsucc).
We prove the intermediate claim HepsPos: Rlt 0 (eps_ (ordsucc (p 0))).
An exact proof term for the current goal is (RltI 0 (eps_ (ordsucc (p 0))) real_0 HepsR HepsPosS).
We prove the intermediate claim HbInMT: open_ball X d x0 (eps_ (ordsucc (p 0))) ∈ metric_topology X d.
An exact proof term for the current goal is (open_ball_in_metric_topology X d x0 (eps_ (ordsucc (p 0))) Hd Hx0X HepsPos).
rewrite the current goal using HbEq (from left to right).
rewrite the current goal using HbBall (from left to right).
rewrite the current goal using HTdef (from left to right).
An exact proof term for the current goal is HbInMT.
We prove the intermediate claim HBasisEq: basis_on X B ∧ generated_topology X B = Tx.
An exact proof term for the current goal is (basis_refines_topology X Tx B HTx HBopen HBref).
We prove the intermediate claim HBgenerates: basis_generates X B Tx.
An exact proof term for the current goal is HBasisEq.
We use B to witness the existential quantifier.
We will prove basis_on X B ∧ countable_set B ∧ basis_generates X B Tx.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is (andEL (basis_on X B) (generated_topology X B = Tx) HBgenerates).
An exact proof term for the current goal is HBcount.
An exact proof term for the current goal is HBgenerates.
∎