Let X, d, x and r be given.
Assume Hm: metric_on X d.
Assume Hx: x ∈ X.
Assume Hr: Rlt 0 r.
Set B to be the term famunion X (λx0 ⇒ {open_ball X d x0 rr|rr ∈ R, Rlt 0 rr}).
We prove the intermediate claim HBasis: basis_on X B.
An exact proof term for the current goal is (open_balls_form_basis X d Hm).
We prove the intermediate claim Hball_in_rfam: open_ball X d x r ∈ {open_ball X d x rr|rr ∈ R, Rlt 0 rr}.
We prove the intermediate claim HrR: r ∈ R.
An exact proof term for the current goal is (RltE_right 0 r Hr).
An exact proof term for the current goal is (ReplSepI R (λrr : set ⇒ Rlt 0 rr) (λrr : set ⇒ open_ball X d x rr) r HrR Hr).
We prove the intermediate claim Hball_in_B: open_ball X d x r ∈ B.
An exact proof term for the current goal is (famunionI X (λx0 ⇒ {open_ball X d x0 rr|rr ∈ R, Rlt 0 rr}) x (open_ball X d x r) Hx Hball_in_rfam).
We prove the intermediate claim HT: topology_on X (metric_topology X d).
An exact proof term for the current goal is (metric_topology_is_topology X d Hm).
We will prove topology_on X (metric_topology X d) ∧ open_ball X d x r ∈ metric_topology X d.
Apply andI to the current goal.
An exact proof term for the current goal is HT.
We will prove open_ball X d x r ∈ metric_topology X d.
We will prove open_ball X d x r ∈ generated_topology X B.
An exact proof term for the current goal is (generated_topology_contains_basis X B HBasis (open_ball X d x r) Hball_in_B).
∎