Let X, d, B and x 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.
Assume HxX: x ∈ X.
Set Tx to be the term metric_topology X d.
We prove the intermediate claim Hcov: covers X B.
An exact proof term for the current goal is (andER (∀b0 : set, b0 ∈ B → b0 ∈ Tx) (covers X B) HBcov).
We prove the intermediate claim Hexb: ∃b : set, b ∈ B ∧ x ∈ b.
An exact proof term for the current goal is (Hcov x HxX).
Apply Hexb to the current goal.
Let b be given.
Assume Hxb: b ∈ B ∧ x ∈ b.
We prove the intermediate claim HbB: b ∈ B.
An exact proof term for the current goal is (andEL (b ∈ B) (x ∈ b) Hxb).
We prove the intermediate claim Hxinb: x ∈ b.
An exact proof term for the current goal is (andER (b ∈ B) (x ∈ b) Hxb).
We prove the intermediate claim Hexcr: ∃c ∈ X, ∃r ∈ R, Rlt 0 r ∧ b = open_ball X d c r.
An exact proof term for the current goal is (HBballs b HbB).
Apply Hexcr to the current goal.
Let c be given.
Assume Hcpack.
We prove the intermediate claim HcX: c ∈ X.
An exact proof term for the current goal is (andEL (c ∈ X) (∃r ∈ R, Rlt 0 r ∧ b = open_ball X d c r) Hcpack).
We prove the intermediate claim Hexr: ∃r ∈ R, Rlt 0 r ∧ b = open_ball X d c r.
An exact proof term for the current goal is (andER (c ∈ X) (∃r ∈ R, Rlt 0 r ∧ b = open_ball X d c r) Hcpack).
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 c r) Hrpack).
We prove the intermediate claim Hrrest: Rlt 0 r ∧ b = open_ball X d c r.
An exact proof term for the current goal is (andER (r ∈ R) (Rlt 0 r ∧ b = open_ball X d c r) Hrpack).
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 c r) Hrrest).
We prove the intermediate claim Hbeq: b = open_ball X d c r.
An exact proof term for the current goal is (andER (Rlt 0 r) (b = open_ball X d c r) Hrrest).
We prove the intermediate claim HxinBall: x ∈ open_ball X d c r.
rewrite the current goal using Hbeq (from right to left).
An exact proof term for the current goal is Hxinb.
We prove the intermediate claim HexN: ∃N : set, N ∈ ω ∧ open_ball X d x (eps_ N) ⊆ open_ball X d c r.
An exact proof term for the current goal is (open_ball_refine_center_eps X d c x r Hm HcX HxX HrR Hrpos HxinBall).
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 ∈ ω) (open_ball X d x (eps_ N) ⊆ open_ball X d c r) HNpair).
We prove the intermediate claim Hsub: open_ball X d x (eps_ N) ⊆ open_ball X d c r.
An exact proof term for the current goal is (andER (N ∈ ω) (open_ball X d x (eps_ N) ⊆ open_ball X d c r) HNpair).
We use b 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 HbB.
An exact proof term for the current goal is Hxinb.
We use N to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HNomega.
rewrite the current goal using Hbeq (from left to right).
An exact proof term for the current goal is Hsub.
∎