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 → ∃x ∈ X, ∃r ∈ R, Rlt 0 r ∧ b = open_ball X d x r.
We will prove ∃V : set, open_cover X (metric_topology X d) V ∧ sigma_locally_finite_family X (metric_topology X d) V ∧ refine_of V B.
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).
We prove the intermediate claim Hneed: ∃Fams : set, countable_set Fams ∧ Fams ⊆ 𝒫 (𝒫 X) ∧ (∀G : set, G ∈ Fams → locally_finite_family X Tx G) ∧ ∃V : set, V = ⋃ Fams ∧ open_cover X Tx V ∧ refine_of V B.
An exact proof term for the current goal is (metric_ball_open_cover_has_sigma_locally_finite_refinement_core_wo X d B Hm HBcov HBballs).
Apply Hneed to the current goal.
Let Fams be given.
Assume HFams.
Apply HFams to the current goal.
Assume HFamsCore HexV.
Apply HFamsCore to the current goal.
Assume HFamsCore2 HFamsLF.
Apply HFamsCore2 to the current goal.
Assume HFamsCnt HFamsSub.
Apply HexV to the current goal.
Let V be given.
Assume HVpack.
Apply HVpack to the current goal.
Assume HVcore HVref.
Apply HVcore to the current goal.
Assume HVeq HVcov.
We use V to witness the existential quantifier.
We will prove open_cover X Tx V ∧ sigma_locally_finite_family X Tx V ∧ refine_of V B.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HVcov.
We will prove sigma_locally_finite_family X Tx V.
We will prove topology_on X Tx ∧ ∃Fams0 : set, countable_set Fams0 ∧ Fams0 ⊆ 𝒫 (𝒫 X) ∧ (∀G : set, G ∈ Fams0 → locally_finite_family X Tx G) ∧ V = ⋃ Fams0.
Apply andI to the current goal.
An exact proof term for the current goal is HTx.
We use Fams to witness the existential quantifier.
We will prove countable_set Fams ∧ Fams ⊆ 𝒫 (𝒫 X) ∧ (∀G : set, G ∈ Fams → locally_finite_family X Tx G) ∧ V = ⋃ Fams.
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 HFamsCnt.
An exact proof term for the current goal is HFamsSub.
An exact proof term for the current goal is HFamsLF.
An exact proof term for the current goal is HVeq.
An exact proof term for the current goal is HVref.
∎