Let X, d and B be given.
Assume Hm: metric_on X d.
Assume HBcov: open_cover X (metric_topology X d) B.
Assume HBballs: ∀b : set, b ∈ B → ∃c ∈ X, ∃r ∈ R, Rlt 0 r ∧ b = open_ball X d c r.
Set Tx to be the term metric_topology X d.
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 Hm).
Set pickb to be the term λx : set ⇒ Eps_i (λb : set ⇒ b ∈ B ∧ x ∈ b ∧ ∃N : set, N ∈ ω ∧ open_ball X d x (eps_ N) ⊆ b).
We prove the intermediate claim Hpickb: ∀x : set, x ∈ X → pickb x ∈ B ∧ x ∈ pickb x ∧ ∃N : set, N ∈ ω ∧ open_ball X d x (eps_ N) ⊆ pickb x.
Let x be given.
Assume HxX: x ∈ X.
We prove the intermediate claim Hex: ∃b : set, b ∈ B ∧ x ∈ b ∧ ∃N : set, N ∈ ω ∧ open_ball X d x (eps_ N) ⊆ b.
An exact proof term for the current goal is (metric_ball_cover_point_eps_submember X d B x Hm HBcov HBballs HxX).
Apply Hex to the current goal.
Let b be given.
Assume Hb: b ∈ B ∧ x ∈ b ∧ ∃N : set, N ∈ ω ∧ open_ball X d x (eps_ N) ⊆ b.
An exact proof term for the current goal is (Eps_i_ax (λb0 : set ⇒ b0 ∈ B ∧ x ∈ b0 ∧ ∃N : set, N ∈ ω ∧ open_ball X d x (eps_ N) ⊆ b0) b Hb).
Set pickN to be the term λx : set ⇒ Eps_i (λN : set ⇒ N ∈ ω ∧ open_ball X d x (eps_ N) ⊆ pickb x).
We prove the intermediate claim HpickN: ∀x : set, x ∈ X → pickN x ∈ ω ∧ open_ball X d x (eps_ (pickN x)) ⊆ pickb x.
Let x be given.
Assume HxX: x ∈ X.
We prove the intermediate claim Hbpack: pickb x ∈ B ∧ x ∈ pickb x ∧ ∃N : set, N ∈ ω ∧ open_ball X d x (eps_ N) ⊆ pickb x.
An exact proof term for the current goal is (Hpickb x HxX).
We prove the intermediate claim Hbcore: (pickb x ∈ B ∧ x ∈ pickb x) ∧ ∃N : set, N ∈ ω ∧ open_ball X d x (eps_ N) ⊆ pickb x.
An exact proof term for the current goal is Hbpack.
We prove the intermediate claim HexN: ∃N : set, N ∈ ω ∧ open_ball X d x (eps_ N) ⊆ pickb x.
An exact proof term for the current goal is (andER (pickb x ∈ B ∧ x ∈ pickb x) (∃N : set, N ∈ ω ∧ open_ball X d x (eps_ N) ⊆ pickb x) Hbcore).
Apply HexN to the current goal.
Let N be given.
Assume HNpair: N ∈ ω ∧ open_ball X d x (eps_ N) ⊆ pickb x.
An exact proof term for the current goal is (Eps_i_ax (λN0 : set ⇒ N0 ∈ ω ∧ open_ball X d x (eps_ N0) ⊆ pickb x) N HNpair).
Set pickV to be the term λx : set ⇒ open_ball X d x (eps_ (pickN x)).
Set V to be the term Repl X (λx : set ⇒ pickV x).
We prove the intermediate claim HVT: ∀v : set, v ∈ V → v ∈ Tx.
Let v be given.
Assume Hv: v ∈ V.
Apply (ReplE X (λx0 : set ⇒ pickV x0) v Hv) to the current goal.
Let x be given.
Assume Hx: x ∈ X ∧ v = pickV x.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (andEL (x ∈ X) (v = pickV x) Hx).
We prove the intermediate claim Heq: v = pickV x.
An exact proof term for the current goal is (andER (x ∈ X) (v = pickV x) Hx).
rewrite the current goal using Heq (from left to right).
We prove the intermediate claim HNpack: pickN x ∈ ω ∧ open_ball X d x (eps_ (pickN x)) ⊆ pickb x.
An exact proof term for the current goal is (HpickN x HxX).
We prove the intermediate claim HNomega: pickN x ∈ ω.
An exact proof term for the current goal is (andEL (pickN x ∈ ω) (open_ball X d x (eps_ (pickN x)) ⊆ pickb x) HNpack).
We prove the intermediate claim HepsPosS: 0 < eps_ (pickN x).
An exact proof term for the current goal is (SNo_eps_pos (pickN x) HNomega).
We prove the intermediate claim HepsR: eps_ (pickN x) ∈ R.
An exact proof term for the current goal is (SNoS_omega_real (eps_ (pickN x)) (SNo_eps_SNoS_omega (pickN x) HNomega)).
We prove the intermediate claim HepsPos: Rlt 0 (eps_ (pickN x)).
An exact proof term for the current goal is (RltI 0 (eps_ (pickN x)) real_0 HepsR HepsPosS).
An exact proof term for the current goal is (open_ball_in_metric_topology X d x (eps_ (pickN x)) Hm HxX HepsPos).
We prove the intermediate claim Hcovers: covers X V.
Let x be given.
Assume HxX: x ∈ X.
We will prove ∃v : set, v ∈ V ∧ x ∈ v.
Set v to be the term pickV x.
We use v to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (ReplI X (λx0 : set ⇒ pickV x0) x HxX).
We prove the intermediate claim HNpack: pickN x ∈ ω ∧ open_ball X d x (eps_ (pickN x)) ⊆ pickb x.
An exact proof term for the current goal is (HpickN x HxX).
We prove the intermediate claim HNomega: pickN x ∈ ω.
An exact proof term for the current goal is (andEL (pickN x ∈ ω) (open_ball X d x (eps_ (pickN x)) ⊆ pickb x) HNpack).
We prove the intermediate claim HepsPosS: 0 < eps_ (pickN x).
An exact proof term for the current goal is (SNo_eps_pos (pickN x) HNomega).
We prove the intermediate claim HepsR: eps_ (pickN x) ∈ R.
An exact proof term for the current goal is (SNoS_omega_real (eps_ (pickN x)) (SNo_eps_SNoS_omega (pickN x) HNomega)).
We prove the intermediate claim HepsPos: Rlt 0 (eps_ (pickN x)).
An exact proof term for the current goal is (RltI 0 (eps_ (pickN x)) real_0 HepsR HepsPosS).
An exact proof term for the current goal is (center_in_open_ball X d x (eps_ (pickN x)) Hm HxX HepsPos).
We prove the intermediate claim Hopen_cover: open_cover X Tx V.
We will prove (∀v0 : set, v0 ∈ V → v0 ∈ Tx) ∧ covers X V.
Apply andI to the current goal.
An exact proof term for the current goal is HVT.
An exact proof term for the current goal is Hcovers.
We prove the intermediate claim Href: refine_of V B.
Let v be given.
Assume Hv: v ∈ V.
We will prove ∃b : set, b ∈ B ∧ v ⊆ b.
Apply (ReplE X (λx0 : set ⇒ pickV x0) v Hv) to the current goal.
Let x be given.
Assume Hx: x ∈ X ∧ v = pickV x.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (andEL (x ∈ X) (v = pickV x) Hx).
We prove the intermediate claim Heq: v = pickV x.
An exact proof term for the current goal is (andER (x ∈ X) (v = pickV x) Hx).
rewrite the current goal using Heq (from left to right).
We prove the intermediate claim Hbpack: pickb x ∈ B ∧ x ∈ pickb x ∧ ∃N : set, N ∈ ω ∧ open_ball X d x (eps_ N) ⊆ pickb x.
An exact proof term for the current goal is (Hpickb x HxX).
We prove the intermediate claim Hb12: pickb x ∈ B ∧ x ∈ pickb x.
An exact proof term for the current goal is (andEL (pickb x ∈ B ∧ x ∈ pickb x) (∃N : set, N ∈ ω ∧ open_ball X d x (eps_ N) ⊆ pickb x) Hbpack).
We prove the intermediate claim HbB: pickb x ∈ B.
An exact proof term for the current goal is (andEL (pickb x ∈ B) (x ∈ pickb x) Hb12).
We prove the intermediate claim HNpack: pickN x ∈ ω ∧ open_ball X d x (eps_ (pickN x)) ⊆ pickb x.
An exact proof term for the current goal is (HpickN x HxX).
We prove the intermediate claim Hsub: open_ball X d x (eps_ (pickN x)) ⊆ pickb x.
An exact proof term for the current goal is (andER (pickN x ∈ ω) (open_ball X d x (eps_ (pickN x)) ⊆ pickb x) HNpack).
We use (pickb x) to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HbB.
An exact proof term for the current goal is Hsub.
We prove the intermediate claim Hshape: ∀v : set, v ∈ V → ∃x : set, x ∈ X ∧ ∃N : set, N ∈ ω ∧ v = open_ball X d x (eps_ N).
Let v be given.
Assume Hv: v ∈ V.
Apply (ReplE X (λx0 : set ⇒ pickV x0) v Hv) to the current goal.
Let x be given.
Assume Hx: x ∈ X ∧ v = pickV x.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (andEL (x ∈ X) (v = pickV x) Hx).
We prove the intermediate claim Heq: v = pickV x.
An exact proof term for the current goal is (andER (x ∈ X) (v = pickV x) Hx).
We use x to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HxX.
We use (pickN x) to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (andEL (pickN x ∈ ω) (open_ball X d x (eps_ (pickN x)) ⊆ pickb x) (HpickN x HxX)).
rewrite the current goal using Heq (from left to right).
Use reflexivity.
We use V to witness the existential quantifier.
We will prove open_cover X Tx V ∧ refine_of V B ∧ (∀v : set, v ∈ V → ∃x : set, x ∈ X ∧ ∃N : set, N ∈ ω ∧ v = open_ball X d x (eps_ N)).
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is Hopen_cover.
An exact proof term for the current goal is Href.
An exact proof term for the current goal is Hshape.
∎