Let X, d and U be given.
Assume Hm: metric_on X d.
Assume Hcov: open_cover X (metric_topology X d) U.
We will prove ∃B : set, open_cover X (metric_topology X d) B ∧ (∀b : set, b ∈ B → ∃x ∈ X, ∃r ∈ R, Rlt 0 r ∧ b = open_ball X d x r) ∧ refine_of B U.
Set B to be the term {b ∈ 𝒫 X|∃x ∈ X, ∃u : set, u ∈ U ∧ x ∈ u ∧ ∃r ∈ R, Rlt 0 r ∧ b = open_ball X d x r ∧ open_ball X d x r ⊆ u}.
We use B to witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
We will prove open_cover X (metric_topology X d) B.
We will prove (∀b0 : set, b0 ∈ B → b0 ∈ metric_topology X d) ∧ covers X B.
Apply andI to the current goal.
Let b0 be given.
Assume Hb0B: b0 ∈ B.
We prove the intermediate claim Hb0P: b0 ∈ 𝒫 X.
An exact proof term for the current goal is (SepE1 (𝒫 X) (λb1 : set ⇒ ∃x ∈ X, ∃u : set, u ∈ U ∧ x ∈ u ∧ ∃r ∈ R, Rlt 0 r ∧ b1 = open_ball X d x r ∧ open_ball X d x r ⊆ u) b0 Hb0B).
We prove the intermediate claim Hwit: ∃x ∈ X, ∃u : set, u ∈ U ∧ x ∈ u ∧ ∃r ∈ R, Rlt 0 r ∧ b0 = open_ball X d x r ∧ open_ball X d x r ⊆ u.
An exact proof term for the current goal is (SepE2 (𝒫 X) (λb1 : set ⇒ ∃x ∈ X, ∃u : set, u ∈ U ∧ x ∈ u ∧ ∃r ∈ R, Rlt 0 r ∧ b1 = open_ball X d x r ∧ open_ball X d x r ⊆ u) b0 Hb0B).
Apply Hwit to the current goal.
Let x be given.
Assume Hxpack.
Apply Hxpack to the current goal.
Assume HxX: x ∈ X.
Assume Hexu: ∃u : set, u ∈ U ∧ x ∈ u ∧ ∃r ∈ R, Rlt 0 r ∧ b0 = open_ball X d x r ∧ open_ball X d x r ⊆ u.
Apply Hexu to the current goal.
Let u be given.
Assume Hupack.
We prove the intermediate claim Hexr: ∃r ∈ R, Rlt 0 r ∧ b0 = open_ball X d x r ∧ open_ball X d x r ⊆ u.
An exact proof term for the current goal is (andER (u ∈ U ∧ x ∈ u) (∃r ∈ R, Rlt 0 r ∧ b0 = open_ball X d x r ∧ open_ball X d x r ⊆ u) Hupack).
Apply Hexr 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 ∧ b0 = open_ball X d x r ∧ open_ball X d x r ⊆ u) Hrpack).
We prove the intermediate claim Hrrest: Rlt 0 r ∧ b0 = open_ball X d x r ∧ open_ball X d x r ⊆ u.
An exact proof term for the current goal is (andER (r ∈ R) (Rlt 0 r ∧ b0 = open_ball X d x r ∧ open_ball X d x r ⊆ u) Hrpack).
We prove the intermediate claim Hrleft: Rlt 0 r ∧ b0 = open_ball X d x r.
An exact proof term for the current goal is (andEL (Rlt 0 r ∧ b0 = open_ball X d x r) (open_ball X d x r ⊆ u) Hrrest).
We prove the intermediate claim Hrpos: Rlt 0 r.
An exact proof term for the current goal is (andEL (Rlt 0 r) (b0 = open_ball X d x r) Hrleft).
We prove the intermediate claim Hb0eq: b0 = open_ball X d x r.
An exact proof term for the current goal is (andER (Rlt 0 r) (b0 = open_ball X d x r) Hrleft).
rewrite the current goal using Hb0eq (from left to right).
An exact proof term for the current goal is (open_ball_in_metric_topology X d x r Hm HxX Hrpos).
We will prove covers X B.
Let x be given.
Assume HxX: x ∈ X.
We will prove ∃b : set, b ∈ B ∧ x ∈ b.
We prove the intermediate claim Hexu: ∃u : set, u ∈ U ∧ ∃r : set, r ∈ R ∧ (Rlt 0 r ∧ open_ball X d x r ⊆ u).
An exact proof term for the current goal is (metric_open_cover_point_ball_submember X d U x Hm Hcov HxX).
Apply Hexu to the current goal.
Let u be given.
Assume Hupair.
We prove the intermediate claim HuU: u ∈ U.
An exact proof term for the current goal is (andEL (u ∈ U) (∃r : set, r ∈ R ∧ (Rlt 0 r ∧ open_ball X d x r ⊆ u)) Hupair).
We prove the intermediate claim Hexr: ∃r : set, r ∈ R ∧ (Rlt 0 r ∧ open_ball X d x r ⊆ u).
An exact proof term for the current goal is (andER (u ∈ U) (∃r : set, r ∈ R ∧ (Rlt 0 r ∧ open_ball X d x r ⊆ u)) Hupair).
Apply Hexr to the current goal.
Let r be given.
Assume Hrpair.
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) Hrpair).
We prove the intermediate claim Hrrest: 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) Hrpair).
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) Hrrest).
We prove the intermediate claim Hsubu: 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) Hrrest).
We use (open_ball X d x r) to witness the existential quantifier.
Apply andI to the current goal.
We prove the intermediate claim HbPow: open_ball X d x r ∈ 𝒫 X.
An exact proof term for the current goal is (open_ball_in_Power X d x r).
Apply (SepI (𝒫 X) (λb1 : set ⇒ ∃x0 ∈ X, ∃u0 : set, u0 ∈ U ∧ x0 ∈ u0 ∧ ∃r0 ∈ R, Rlt 0 r0 ∧ b1 = open_ball X d x0 r0 ∧ open_ball X d x0 r0 ⊆ u0) (open_ball X d x r) HbPow) to the current goal.
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 u to witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HuU.
We prove the intermediate claim Hxball: x ∈ open_ball X d x r.
An exact proof term for the current goal is (center_in_open_ball X d x r Hm HxX Hrpos).
An exact proof term for the current goal is (Hsubu x Hxball).
We use r to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HrR.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is Hrpos.
Use reflexivity.
An exact proof term for the current goal is Hsubu.
An exact proof term for the current goal is (center_in_open_ball X d x r Hm HxX Hrpos).
Let b be given.
Assume HbB: b ∈ B.
We prove the intermediate claim Hwit: ∃x ∈ X, ∃u : set, u ∈ U ∧ x ∈ u ∧ ∃r ∈ R, Rlt 0 r ∧ b = open_ball X d x r ∧ open_ball X d x r ⊆ u.
An exact proof term for the current goal is (SepE2 (𝒫 X) (λb1 : set ⇒ ∃x ∈ X, ∃u : set, u ∈ U ∧ x ∈ u ∧ ∃r ∈ R, Rlt 0 r ∧ b1 = open_ball X d x r ∧ open_ball X d x r ⊆ u) b HbB).
Apply Hwit to the current goal.
Let x be given.
Assume Hxpack.
Apply Hxpack to the current goal.
Assume HxX: x ∈ X.
Assume Hexu: ∃u : set, u ∈ U ∧ x ∈ u ∧ ∃r ∈ R, Rlt 0 r ∧ b = open_ball X d x r ∧ open_ball X d x r ⊆ u.
Apply Hexu to the current goal.
Let u be given.
Assume Hupack.
We prove the intermediate claim Hexr: ∃r ∈ R, Rlt 0 r ∧ b = open_ball X d x r ∧ open_ball X d x r ⊆ u.
An exact proof term for the current goal is (andER (u ∈ U ∧ x ∈ u) (∃r ∈ R, Rlt 0 r ∧ b = open_ball X d x r ∧ open_ball X d x r ⊆ u) Hupack).
Apply Hexr 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 ∧ b = open_ball X d x r ∧ open_ball X d x r ⊆ u) Hrpack).
We prove the intermediate claim Hrrest: Rlt 0 r ∧ b = open_ball X d x r ∧ open_ball X d x r ⊆ u.
An exact proof term for the current goal is (andER (r ∈ R) (Rlt 0 r ∧ b = open_ball X d x r ∧ open_ball X d x r ⊆ u) Hrpack).
We prove the intermediate claim Hrleft: Rlt 0 r ∧ b = open_ball X d x r.
An exact proof term for the current goal is (andEL (Rlt 0 r ∧ b = open_ball X d x r) (open_ball X d x r ⊆ u) Hrrest).
We prove the intermediate claim Hrpos: Rlt 0 r.
An exact proof term for the current goal is (andEL (Rlt 0 r) (b = open_ball X d x r) Hrleft).
We prove the intermediate claim Hbeq: b = open_ball X d x r.
An exact proof term for the current goal is (andER (Rlt 0 r) (b = open_ball X d x r) Hrleft).
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 r to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HrR.
Apply andI to the current goal.
An exact proof term for the current goal is Hrpos.
An exact proof term for the current goal is Hbeq.
We will prove refine_of B U.
Let b be given.
Assume HbB: b ∈ B.
We will prove ∃u : set, u ∈ U ∧ b ⊆ u.
We prove the intermediate claim Hwit: ∃x ∈ X, ∃u : set, u ∈ U ∧ x ∈ u ∧ ∃r ∈ R, Rlt 0 r ∧ b = open_ball X d x r ∧ open_ball X d x r ⊆ u.
An exact proof term for the current goal is (SepE2 (𝒫 X) (λb1 : set ⇒ ∃x ∈ X, ∃u : set, u ∈ U ∧ x ∈ u ∧ ∃r ∈ R, Rlt 0 r ∧ b1 = open_ball X d x r ∧ open_ball X d x r ⊆ u) b HbB).
Apply Hwit to the current goal.
Let x be given.
Assume Hxpack.
Apply Hxpack to the current goal.
Assume HxX: x ∈ X.
Assume Hexu: ∃u : set, u ∈ U ∧ x ∈ u ∧ ∃r ∈ R, Rlt 0 r ∧ b = open_ball X d x r ∧ open_ball X d x r ⊆ u.
Apply Hexu to the current goal.
Let u be given.
Assume Hupack.
We prove the intermediate claim HuUx: u ∈ U ∧ x ∈ u.
An exact proof term for the current goal is (andEL (u ∈ U ∧ x ∈ u) (∃r ∈ R, Rlt 0 r ∧ b = open_ball X d x r ∧ open_ball X d x r ⊆ u) Hupack).
We prove the intermediate claim HuU: u ∈ U.
An exact proof term for the current goal is (andEL (u ∈ U) (x ∈ u) HuUx).
We prove the intermediate claim Hexr: ∃r ∈ R, Rlt 0 r ∧ b = open_ball X d x r ∧ open_ball X d x r ⊆ u.
An exact proof term for the current goal is (andER (u ∈ U ∧ x ∈ u) (∃r ∈ R, Rlt 0 r ∧ b = open_ball X d x r ∧ open_ball X d x r ⊆ u) Hupack).
Apply Hexr to the current goal.
Let r be given.
Assume Hrpack.
We prove the intermediate claim Hrrest: Rlt 0 r ∧ b = open_ball X d x r ∧ open_ball X d x r ⊆ u.
An exact proof term for the current goal is (andER (r ∈ R) (Rlt 0 r ∧ b = open_ball X d x r ∧ open_ball X d x r ⊆ u) Hrpack).
We prove the intermediate claim Hrleft: Rlt 0 r ∧ b = open_ball X d x r.
An exact proof term for the current goal is (andEL (Rlt 0 r ∧ b = open_ball X d x r) (open_ball X d x r ⊆ u) Hrrest).
We prove the intermediate claim Hsub: open_ball X d x r ⊆ u.
An exact proof term for the current goal is (andER (Rlt 0 r ∧ b = open_ball X d x r) (open_ball X d x r ⊆ u) Hrrest).
We prove the intermediate claim Hbeq: b = open_ball X d x r.
An exact proof term for the current goal is (andER (Rlt 0 r) (b = open_ball X d x r) Hrleft).
We use u to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HuU.
rewrite the current goal using Hbeq (from left to right).
An exact proof term for the current goal is Hsub.
∎