Let X and Tx be given.
Assume Hmet: metrizable X Tx.
Assume HexD: ∃D : set, D ⊆ X ∧ countable D ∧ dense_in D 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).
Apply HexD to the current goal.
Let D be given.
Assume HDall: D ⊆ X ∧ countable D ∧ dense_in D X Tx.
We prove the intermediate claim HDmid: (D ⊆ X ∧ countable D) ∧ dense_in D X Tx.
An exact proof term for the current goal is HDall.
We prove the intermediate claim HDleft: D ⊆ X ∧ countable D.
An exact proof term for the current goal is (andEL (D ⊆ X ∧ countable D) (dense_in D X Tx) HDmid).
We prove the intermediate claim Hdense: dense_in D X Tx.
An exact proof term for the current goal is (andER (D ⊆ X ∧ countable D) (dense_in D X Tx) HDmid).
We prove the intermediate claim HDsubX: D ⊆ X.
An exact proof term for the current goal is (andEL (D ⊆ X) (countable D) HDleft).
We prove the intermediate claim HDcount: countable D.
An exact proof term for the current goal is (andER (D ⊆ X) (countable D) HDleft).
We will prove second_countable_space X Tx.
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.
We will prove topology_on X Tx.
rewrite the current goal using HTdef (from right to left).
An exact proof term for the current goal is (metric_topology_is_topology X d Hm).
Set Y to be the term λ_ : set ⇒ ω of type set → set.
Set Pair to be the term ∑x0 ∈ D, Y x0.
Set F to be the term λz : set ⇒ open_ball X d (z 0) (eps_ (ordsucc (z 1))) of type set → set.
Set B to be the term {F z|z ∈ Pair}.
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 HDcountset: countable_set D.
An exact proof term for the current goal is HDcount.
We prove the intermediate claim HPairCount: countable_set Pair.
Set Y0 to be the term λ_ : set ⇒ ω of type set → set.
We prove the intermediate claim HY0: ∀x0 : set, x0 ∈ D → countable (Y0 x0).
Let x0 be given.
Assume _.
An exact proof term for the current goal is HomegaCount.
An exact proof term for the current goal is (Sigma_countable D HDcountset Y0 HY0).
We prove the intermediate claim HBcount: countable_set B.
An exact proof term for the current goal is (countable_image Pair HPairCount F).
We prove the intermediate claim HTx: topology_on X Tx.
We will prove topology_on X Tx.
rewrite the current goal using HTdef (from right to left).
An exact proof term for the current goal is (metric_topology_is_topology X d Hm).
We prove the intermediate claim HBsub: ∀c ∈ B, c ∈ Tx.
Let c be given.
Assume HcB: c ∈ B.
We will prove c ∈ Tx.
Apply (ReplE_impred Pair F c HcB) to the current goal.
Let z be given.
Assume HzPair: z ∈ Pair.
Assume HcEq: c = F z.
rewrite the current goal using HcEq (from left to right).
Set c0 to be the term z 0.
Set n0 to be the term z 1.
We prove the intermediate claim Hc0D: c0 ∈ D.
An exact proof term for the current goal is (ap0_Sigma D Y z HzPair).
We prove the intermediate claim Hc0X: c0 ∈ X.
An exact proof term for the current goal is (HDsubX c0 Hc0D).
We prove the intermediate claim Hn0Omega: n0 ∈ ω.
An exact proof term for the current goal is (ap1_Sigma D Y z HzPair).
We prove the intermediate claim HsuccOmega: ordsucc n0 ∈ ω.
An exact proof term for the current goal is (omega_ordsucc n0 Hn0Omega).
We prove the intermediate claim HradR: eps_ (ordsucc n0) ∈ R.
An exact proof term for the current goal is (SNoS_omega_real (eps_ (ordsucc n0)) (SNo_eps_SNoS_omega (ordsucc n0) HsuccOmega)).
We prove the intermediate claim HradposS: 0 < eps_ (ordsucc n0).
An exact proof term for the current goal is (SNo_eps_pos (ordsucc n0) HsuccOmega).
We prove the intermediate claim Hradpos: Rlt 0 (eps_ (ordsucc n0)).
An exact proof term for the current goal is (RltI 0 (eps_ (ordsucc n0)) real_0 HradR HradposS).
We prove the intermediate claim HballIn: open_ball X d c0 (eps_ (ordsucc n0)) ∈ metric_topology X d.
An exact proof term for the current goal is (open_ball_in_metric_topology X d c0 (eps_ (ordsucc n0)) Hm Hc0X Hradpos).
rewrite the current goal using HTdef (from right to left).
An exact proof term for the current goal is HballIn.
We prove the intermediate claim HBrefines: ∀U ∈ Tx, ∀x ∈ U, ∃Cx ∈ B, x ∈ Cx ∧ Cx ⊆ U.
Let U be given.
Assume HU: U ∈ Tx.
Let x be given.
Assume HxU: x ∈ U.
We will prove ∃Cx ∈ B, x ∈ Cx ∧ Cx ⊆ U.
We prove the intermediate claim HTsub: Tx ⊆ 𝒫 X.
An exact proof term for the current goal is (topology_subset_axiom X Tx HTx).
We prove the intermediate claim HUpow: U ∈ 𝒫 X.
An exact proof term for the current goal is (HTsub 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 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).
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.
Set Ux to be the term open_ball X d x s.
We prove the intermediate claim HUxInTx: Ux ∈ Tx.
We will prove Ux ∈ Tx.
rewrite the current goal using HTdef (from right to left).
An exact proof term for the current goal is (open_ball_in_metric_topology X d x s Hm HxX Hspos).
We prove the intermediate claim HUxNe: Ux ≠ Empty.
An exact proof term for the current goal is (open_ball_nonempty X d x s Hm HxX Hspos).
We prove the intermediate claim HmeetNe: Ux ∩ D ≠ Empty.
An exact proof term for the current goal is (dense_in_meets_nonempty_open D X Tx Ux HTx Hdense HUxInTx HUxNe).
We prove the intermediate claim Hexd0: ∃d0 : set, d0 ∈ Ux ∩ D.
An exact proof term for the current goal is (nonempty_has_element (Ux ∩ D) HmeetNe).
Apply Hexd0 to the current goal.
Let d0 be given.
Assume Hd0cap: d0 ∈ Ux ∩ D.
We prove the intermediate claim Hd0Ux: d0 ∈ Ux.
An exact proof term for the current goal is (binintersectE1 Ux D d0 Hd0cap).
We prove the intermediate claim Hd0D: d0 ∈ D.
An exact proof term for the current goal is (binintersectE2 Ux D d0 Hd0cap).
We prove the intermediate claim Hd0X: d0 ∈ X.
An exact proof term for the current goal is (HDsubX d0 Hd0D).
Set Cx to be the term open_ball X d d0 s.
We use Cx to witness the existential quantifier.
We will prove Cx ∈ B ∧ (x ∈ Cx ∧ Cx ⊆ U).
Apply andI to the current goal.
We prove the intermediate claim HNinY: N ∈ Y d0.
An exact proof term for the current goal is HNomega.
We prove the intermediate claim HpSig: (d0,N) ∈ Pair.
An exact proof term for the current goal is (tuple_2_Sigma D Y d0 Hd0D N HNinY).
We prove the intermediate claim HF: F (d0,N) = Cx.
We will prove F (d0,N) = Cx.
We prove the intermediate claim HCxDef: Cx = open_ball X d d0 s.
Use reflexivity.
rewrite the current goal using HCxDef (from left to right).
rewrite the current goal using HsDef (from left to right).
We prove the intermediate claim HFdef: F (d0,N) = open_ball X d ((d0,N) 0) (eps_ (ordsucc ((d0,N) 1))).
Use reflexivity.
rewrite the current goal using HFdef (from left to right).
rewrite the current goal using (tuple_2_0_eq d0 N) (from left to right).
rewrite the current goal using (tuple_2_1_eq d0 N) (from left to right).
Use reflexivity.
rewrite the current goal using HF (from right to left).
An exact proof term for the current goal is (ReplI Pair F (d0,N) HpSig).
Apply andI to the current goal.
We prove the intermediate claim Hd0inBall: d0 ∈ open_ball X d x s.
rewrite the current goal using HsDef (from right to left).
An exact proof term for the current goal is Hd0Ux.
We prove the intermediate claim Hdxd0: Rlt (apply_fun d (x,d0)) s.
An exact proof term for the current goal is (open_ballE2 X d x s d0 Hd0inBall).
We prove the intermediate claim Hsym: apply_fun d (d0,x) = apply_fun d (x,d0).
An exact proof term for the current goal is (metric_on_symmetric X d d0 x Hm Hd0X HxX).
We prove the intermediate claim Hdx0: Rlt (apply_fun d (d0,x)) s.
rewrite the current goal using Hsym (from left to right).
An exact proof term for the current goal is Hdxd0.
An exact proof term for the current goal is (open_ballI X d d0 s x HxX Hdx0).
We prove the intermediate claim HsubBall: Cx ⊆ open_ball X d x r.
Let y be given.
Assume Hy: y ∈ Cx.
We will prove y ∈ open_ball X d x r.
We prove the intermediate claim HyX: y ∈ X.
An exact proof term for the current goal is (open_ballE1 X d d0 s y Hy).
We prove the intermediate claim Hdy: Rlt (apply_fun d (d0,y)) s.
An exact proof term for the current goal is (open_ballE2 X d d0 s y Hy).
We prove the intermediate claim Hd0inBall: d0 ∈ open_ball X d x s.
rewrite the current goal using HsDef (from right to left).
An exact proof term for the current goal is Hd0Ux.
We prove the intermediate claim Hdx: Rlt (apply_fun d (x,d0)) s.
An exact proof term for the current goal is (open_ballE2 X d x s d0 Hd0inBall).
Set dx to be the term apply_fun d (x,d0).
Set dy to be the term apply_fun d (d0,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 Hm).
We prove the intermediate claim HdxR: dx ∈ R.
An exact proof term for the current goal is (HdFun (x,d0) (tuple_2_setprod_by_pair_Sigma X X x d0 HxX Hd0X)).
We prove the intermediate claim HdyR: dy ∈ R.
An exact proof term for the current goal is (HdFun (d0,y) (tuple_2_setprod_by_pair_Sigma X X d0 y Hd0X 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.
An exact proof term for the current goal is (RltE_lt dx s Hdx).
We prove the intermediate claim HdyLtS: dy < s.
An exact proof term for the current goal is (RltE_lt dy s 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 will prove 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,d0)) (apply_fun d (d0,y))).
An exact proof term for the current goal is (metric_triangle_Rle X d x d0 y Hm HxX Hd0X HyX).
Set tmp2 to be the term add_SNo (apply_fun d (x,d0)) (apply_fun d (d0,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 Cx (open_ball X d x r) U HsubBall Hballsub).
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 HBsub HBrefines).
We prove the intermediate claim HBgenerates: basis_generates X B Tx.
We will prove basis_on X B ∧ generated_topology X B = Tx.
An exact proof term for the current goal is HBasisEq.
We prove the intermediate claim HBasis: basis_on X B.
An exact proof term for the current goal is (andEL (basis_on X B) (generated_topology X B = Tx) 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.
An exact proof term for the current goal is (andI (basis_on X B) (countable_set B) HBasis HBcount).
An exact proof term for the current goal is HBgenerates.
∎