Let X, d and A be given.
Assume Hd: metric_on X d.
Assume HA: A ⊆ X.
Set dA to be the term metric_restrict X d A.
Set TA to be the term metric_topology A dA.
Set Tx to be the term metric_topology X d.
Set BA to be the term famunion A (λx0 : set ⇒ {open_ball A dA x0 r|r ∈ R, Rlt 0 r}).
Set Bx to be the term famunion X (λx0 : set ⇒ {open_ball X d x0 r|r ∈ R, Rlt 0 r}).
We prove the intermediate claim HdA: metric_on A dA.
An exact proof term for the current goal is (metric_restrict_is_metric_on X d A Hd HA).
We prove the intermediate claim HTx: topology_on X Tx.
An exact proof term for the current goal is (metric_topology_is_topology X d Hd).
We prove the intermediate claim HTA: topology_on A TA.
An exact proof term for the current goal is (metric_topology_is_topology A dA HdA).
We prove the intermediate claim HTsub: topology_on A (subspace_topology X Tx A).
An exact proof term for the current goal is (subspace_topology_is_topology X Tx A HTx HA).
We prove the intermediate claim HTA_sub: TA ⊆ subspace_topology X Tx A.
We prove the intermediate claim HallBA: ∀b ∈ BA, b ∈ subspace_topology X Tx A.
Let b be given.
Assume HbBA: b ∈ BA.
We will prove b ∈ subspace_topology X Tx A.
Apply (famunionE_impred A (λx0 : set ⇒ {open_ball A dA x0 r|r ∈ R, Rlt 0 r}) b HbBA (b ∈ subspace_topology X Tx A)) to the current goal.
Let x0 be given.
Assume Hx0A: x0 ∈ A.
Assume HbIn: b ∈ {open_ball A dA x0 r|r ∈ R, Rlt 0 r}.
Apply (ReplSepE_impred R (λr0 : set ⇒ Rlt 0 r0) (λr0 : set ⇒ open_ball A dA x0 r0) b HbIn (b ∈ subspace_topology X Tx A)) to the current goal.
Let r0 be given.
Assume Hr0R: r0 ∈ R.
Assume Hr0pos: Rlt 0 r0.
Assume Hbeq: b = open_ball A dA x0 r0.
rewrite the current goal using Hbeq (from left to right).
We prove the intermediate claim Hx0X: x0 ∈ X.
An exact proof term for the current goal is (HA x0 Hx0A).
We prove the intermediate claim HballIn: open_ball X d x0 r0 ∈ {open_ball X d x0 r|r ∈ R, Rlt 0 r}.
An exact proof term for the current goal is (ReplSepI R (λr1 : set ⇒ Rlt 0 r1) (λr1 : set ⇒ open_ball X d x0 r1) r0 Hr0R Hr0pos).
We prove the intermediate claim HballInFam: open_ball X d x0 r0 ∈ Bx.
An exact proof term for the current goal is (famunionI X (λc0 : set ⇒ {open_ball X d c0 r|r ∈ R, Rlt 0 r}) x0 (open_ball X d x0 r0) Hx0X HballIn).
We prove the intermediate claim HBx: basis_on X Bx.
An exact proof term for the current goal is (open_balls_form_basis X d Hd).
We prove the intermediate claim HballOpen: open_ball X d x0 r0 ∈ Tx.
rewrite the current goal using (metric_topology_generated_by_balls X d Hd) (from right to left).
An exact proof term for the current goal is (generated_topology_contains_basis X Bx HBx (open_ball X d x0 r0) HballInFam).
We prove the intermediate claim HballEq: open_ball A dA x0 r0 = (open_ball X d x0 r0) ∩ A.
Apply set_ext to the current goal.
Let y be given.
Assume Hy: y ∈ open_ball A dA x0 r0.
We will prove y ∈ (open_ball X d x0 r0) ∩ A.
We prove the intermediate claim HyA: y ∈ A.
An exact proof term for the current goal is (open_ballE1 A dA x0 r0 y Hy).
We prove the intermediate claim HyX: y ∈ X.
An exact proof term for the current goal is (HA y HyA).
We prove the intermediate claim Hylt: Rlt (apply_fun dA (x0,y)) r0.
An exact proof term for the current goal is (open_ballE2 A dA x0 r0 y Hy).
We prove the intermediate claim HyltX: Rlt (apply_fun d (x0,y)) r0.
rewrite the current goal using (metric_restrict_apply X d A x0 y Hx0A HyA) (from right to left).
An exact proof term for the current goal is Hylt.
We prove the intermediate claim HyBallX: y ∈ open_ball X d x0 r0.
An exact proof term for the current goal is (open_ballI X d x0 r0 y HyX HyltX).
An exact proof term for the current goal is (binintersectI (open_ball X d x0 r0) A y HyBallX HyA).
Let y be given.
Assume Hy: y ∈ (open_ball X d x0 r0) ∩ A.
We will prove y ∈ open_ball A dA x0 r0.
We prove the intermediate claim HyBallX: y ∈ open_ball X d x0 r0.
An exact proof term for the current goal is (binintersectE1 (open_ball X d x0 r0) A y Hy).
We prove the intermediate claim HyA: y ∈ A.
An exact proof term for the current goal is (binintersectE2 (open_ball X d x0 r0) A y Hy).
We prove the intermediate claim HyltX: Rlt (apply_fun d (x0,y)) r0.
An exact proof term for the current goal is (open_ballE2 X d x0 r0 y HyBallX).
We prove the intermediate claim HyltA: Rlt (apply_fun dA (x0,y)) r0.
rewrite the current goal using (metric_restrict_apply X d A x0 y Hx0A HyA) (from left to right).
An exact proof term for the current goal is HyltX.
An exact proof term for the current goal is (open_ballI A dA x0 r0 y HyA HyltA).
rewrite the current goal using HballEq (from left to right).
An exact proof term for the current goal is (subspace_topologyI X Tx A (open_ball X d x0 r0) HballOpen).
We prove the intermediate claim HsubIncl: generated_topology A BA ⊆ subspace_topology X Tx A.
An exact proof term for the current goal is (generated_topology_finer_weak A BA (subspace_topology X Tx A) HTsub HallBA).
rewrite the current goal using (metric_topology_generated_by_balls A dA HdA) (from right to left).
An exact proof term for the current goal is HsubIncl.
We prove the intermediate claim Hsub_TA: subspace_topology X Tx A ⊆ TA.
We prove the intermediate claim HBx_pair: basis_on X Bx ∧ generated_topology X Bx = Tx.
Apply andI to the current goal.
An exact proof term for the current goal is (open_balls_form_basis X d Hd).
rewrite the current goal using (metric_topology_generated_by_balls X d Hd) (from left to right).
Use reflexivity.
We prove the intermediate claim HsubBasis: basis_on A {b ∩ A|b ∈ Bx} ∧ generated_topology A {b ∩ A|b ∈ Bx} = subspace_topology X Tx A.
An exact proof term for the current goal is (subspace_basis X Tx A Bx HTx HA HBx_pair).
We prove the intermediate claim HsubEq: generated_topology A {b ∩ A|b ∈ Bx} = subspace_topology X Tx A.
An exact proof term for the current goal is (andER (basis_on A {b ∩ A|b ∈ Bx}) (generated_topology A {b ∩ A|b ∈ Bx} = subspace_topology X Tx A) HsubBasis).
rewrite the current goal using HsubEq (from right to left).
We prove the intermediate claim HallC: ∀c ∈ {b ∩ A|b ∈ Bx}, c ∈ TA.
Let c be given.
Assume HcC: c ∈ {b ∩ A|b ∈ Bx}.
We will prove c ∈ TA.
We prove the intermediate claim Hexb: ∃b0 ∈ Bx, c = b0 ∩ A.
An exact proof term for the current goal is (ReplE Bx (λb0 : set ⇒ b0 ∩ A) c HcC).
Apply Hexb to the current goal.
Let b0 be given.
Assume Hb0pair.
We prove the intermediate claim Hb0Bx: b0 ∈ Bx.
An exact proof term for the current goal is (andEL (b0 ∈ Bx) (c = b0 ∩ A) Hb0pair).
We prove the intermediate claim Hceq: c = b0 ∩ A.
An exact proof term for the current goal is (andER (b0 ∈ Bx) (c = b0 ∩ A) Hb0pair).
Apply (famunionE_impred X (λx0 : set ⇒ {open_ball X d x0 r|r ∈ R, Rlt 0 r}) b0 Hb0Bx (c ∈ TA)) to the current goal.
Let x0 be given.
Assume Hx0X: x0 ∈ X.
Assume Hb0In: b0 ∈ {open_ball X d x0 r|r ∈ R, Rlt 0 r}.
Apply (ReplSepE_impred R (λr0 : set ⇒ Rlt 0 r0) (λr0 : set ⇒ open_ball X d x0 r0) b0 Hb0In (c ∈ TA)) to the current goal.
Let r0 be given.
Assume Hr0R: r0 ∈ R.
Assume Hr0pos: Rlt 0 r0.
Assume Hb0eq: b0 = open_ball X d x0 r0.
rewrite the current goal using Hceq (from left to right).
rewrite the current goal using Hb0eq (from left to right).
rewrite the current goal using (metric_topology_generated_by_balls A dA HdA) (from right to left).
We will prove open_ball X d x0 r0 ∩ A ∈ generated_topology A BA.
We prove the intermediate claim HgenDef: generated_topology A BA = {U0 ∈ 𝒫 A|∀y ∈ U0, ∃bA ∈ BA, y ∈ bA ∧ bA ⊆ U0}.
Use reflexivity.
rewrite the current goal using HgenDef (from left to right).
Apply (SepI (𝒫 A) (λU0 : set ⇒ ∀y ∈ U0, ∃bA ∈ BA, y ∈ bA ∧ bA ⊆ U0) (open_ball X d x0 r0 ∩ A)) to the current goal.
Apply PowerI to the current goal.
An exact proof term for the current goal is (binintersect_Subq_2 (open_ball X d x0 r0) A).
Let y be given.
Assume Hy: y ∈ open_ball X d x0 r0 ∩ A.
We will prove ∃bA ∈ BA, y ∈ bA ∧ bA ⊆ open_ball X d x0 r0 ∩ A.
We prove the intermediate claim HyBallX: y ∈ open_ball X d x0 r0.
An exact proof term for the current goal is (binintersectE1 (open_ball X d x0 r0) A y Hy).
We prove the intermediate claim HyA: y ∈ A.
An exact proof term for the current goal is (binintersectE2 (open_ball X d x0 r0) A y Hy).
We prove the intermediate claim HyX: y ∈ X.
An exact proof term for the current goal is (HA y HyA).
We prove the intermediate claim Hexs: ∃s : set, s ∈ R ∧ Rlt 0 s ∧ open_ball X d y s ⊆ open_ball X d x0 r0.
An exact proof term for the current goal is (open_ball_refine_center X d x0 y r0 Hd Hx0X HyX Hr0R Hr0pos HyBallX).
Apply Hexs to the current goal.
Let s be given.
Assume Hs.
We prove the intermediate claim Hs12: s ∈ R ∧ Rlt 0 s.
An exact proof term for the current goal is (andEL (s ∈ R ∧ Rlt 0 s) (open_ball X d y s ⊆ open_ball X d x0 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) Hs12).
We prove the intermediate claim Hspos: Rlt 0 s.
An exact proof term for the current goal is (andER (s ∈ R) (Rlt 0 s) Hs12).
We prove the intermediate claim HsSub: open_ball X d y s ⊆ open_ball X d x0 r0.
An exact proof term for the current goal is (andER (s ∈ R ∧ Rlt 0 s) (open_ball X d y s ⊆ open_ball X d x0 r0) Hs).
We use (open_ball A dA y s) to witness the existential quantifier.
Apply andI to the current goal.
We prove the intermediate claim HbIn: open_ball A dA y s ∈ {open_ball A dA y r|r ∈ R, Rlt 0 r}.
An exact proof term for the current goal is (ReplSepI R (λr1 : set ⇒ Rlt 0 r1) (λr1 : set ⇒ open_ball A dA y r1) s HsR Hspos).
An exact proof term for the current goal is (famunionI A (λc0 : set ⇒ {open_ball A dA c0 r|r ∈ R, Rlt 0 r}) y (open_ball A dA y s) HyA HbIn).
Apply andI to the current goal.
An exact proof term for the current goal is (center_in_open_ball A dA y s HdA HyA Hspos).
Let z be given.
Assume Hz: z ∈ open_ball A dA y s.
We will prove z ∈ open_ball X d x0 r0 ∩ A.
We prove the intermediate claim HzA: z ∈ A.
An exact proof term for the current goal is (open_ballE1 A dA y s z Hz).
We prove the intermediate claim HzX: z ∈ X.
An exact proof term for the current goal is (HA z HzA).
We prove the intermediate claim HzltA: Rlt (apply_fun dA (y,z)) s.
An exact proof term for the current goal is (open_ballE2 A dA y s z Hz).
We prove the intermediate claim HzltX: Rlt (apply_fun d (y,z)) s.
rewrite the current goal using (metric_restrict_apply X d A y z HyA HzA) (from right to left).
An exact proof term for the current goal is HzltA.
We prove the intermediate claim HzBallY: z ∈ open_ball X d y s.
An exact proof term for the current goal is (open_ballI X d y s z HzX HzltX).
We prove the intermediate claim HzBall0: z ∈ open_ball X d x0 r0.
An exact proof term for the current goal is (HsSub z HzBallY).
An exact proof term for the current goal is (binintersectI (open_ball X d x0 r0) A z HzBall0 HzA).
An exact proof term for the current goal is (generated_topology_finer_weak A {b ∩ A|b ∈ Bx} TA HTA HallC).
Apply set_ext to the current goal.
Let U be given.
Assume HU: U ∈ TA.
An exact proof term for the current goal is (HTA_sub U HU).
Let U be given.
Assume HU: U ∈ subspace_topology X Tx A.
An exact proof term for the current goal is (Hsub_TA U HU).
∎