Let X, Tx, Y, d, f, y and r be given.
Assume HTx: topology_on X Tx.
Assume Hm: metric_on Y d.
Assume Hcont: continuous_map X Tx Y (metric_topology Y d) f.
Assume HyY: y ∈ Y.
Assume HrR: r ∈ R.
Assume HrPos: Rlt 0 r.
Set Ty to be the term metric_topology Y d.
We prove the intermediate claim HTy: topology_on Y Ty.
An exact proof term for the current goal is (metric_topology_is_topology Y d Hm).
We prove the intermediate claim Hfun: function_on f X Y.
An exact proof term for the current goal is (continuous_map_function_on X Tx Y Ty f Hcont).
Let x be given.
Assume Hx: x ∈ closure_of X Tx (preimage_of X f (open_ball Y d y r)).
We will prove x ∈ preimage_of X f (open_ball Y d y (add_SNo r r)).
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (SepE1 X (λx0 : set ⇒ ∀U : set, U ∈ Tx → x0 ∈ U → U ∩ preimage_of X f (open_ball Y d y r) ≠ Empty) x Hx).
We prove the intermediate claim Hclx: ∀U : set, U ∈ Tx → x ∈ U → U ∩ preimage_of X f (open_ball Y d y r) ≠ Empty.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ ∀U : set, U ∈ Tx → x0 ∈ U → U ∩ preimage_of X f (open_ball Y d y r) ≠ Empty) x Hx).
Set fx to be the term apply_fun f x.
We prove the intermediate claim HfxY: fx ∈ Y.
An exact proof term for the current goal is (Hfun x HxX).
We prove the intermediate claim HfxCl: fx ∈ closure_of Y Ty (open_ball Y d y r).
We prove the intermediate claim HdefCl: closure_of Y Ty (open_ball Y d y r) = {z0 ∈ Y|∀V : set, V ∈ Ty → z0 ∈ V → V ∩ open_ball Y d y r ≠ Empty}.
Use reflexivity.
rewrite the current goal using HdefCl (from left to right).
Apply (SepI Y (λz0 : set ⇒ ∀V : set, V ∈ Ty → z0 ∈ V → V ∩ open_ball Y d y r ≠ Empty) fx HfxY) to the current goal.
Let V be given.
Assume HV: V ∈ Ty.
Assume HfxV: fx ∈ V.
We will prove V ∩ open_ball Y d y r ≠ Empty.
We prove the intermediate claim HpreVTx: preimage_of X f V ∈ Tx.
An exact proof term for the current goal is (continuous_map_preimage X Tx Y Ty f Hcont V HV).
We prove the intermediate claim HxPreV: x ∈ preimage_of X f V.
An exact proof term for the current goal is (SepI X (λu : set ⇒ apply_fun f u ∈ V) x HxX HfxV).
We prove the intermediate claim Hmeet: (preimage_of X f V) ∩ preimage_of X f (open_ball Y d y r) ≠ Empty.
An exact proof term for the current goal is (Hclx (preimage_of X f V) HpreVTx HxPreV).
We prove the intermediate claim Hext: ∃t : set, t ∈ (preimage_of X f V) ∩ preimage_of X f (open_ball Y d y r).
An exact proof term for the current goal is (nonempty_has_element ((preimage_of X f V) ∩ preimage_of X f (open_ball Y d y r)) Hmeet).
Apply Hext to the current goal.
Let t be given.
Assume Ht: t ∈ (preimage_of X f V) ∩ preimage_of X f (open_ball Y d y r).
We will prove V ∩ open_ball Y d y r ≠ Empty.
We prove the intermediate claim HtPreV: t ∈ preimage_of X f V.
An exact proof term for the current goal is (binintersectE1 (preimage_of X f V) (preimage_of X f (open_ball Y d y r)) t Ht).
We prove the intermediate claim HtPreB: t ∈ preimage_of X f (open_ball Y d y r).
An exact proof term for the current goal is (binintersectE2 (preimage_of X f V) (preimage_of X f (open_ball Y d y r)) t Ht).
We prove the intermediate claim HtX: t ∈ X.
An exact proof term for the current goal is (SepE1 X (λu : set ⇒ apply_fun f u ∈ V) t HtPreV).
We prove the intermediate claim HftV: apply_fun f t ∈ V.
An exact proof term for the current goal is (SepE2 X (λu : set ⇒ apply_fun f u ∈ V) t HtPreV).
We prove the intermediate claim HftB: apply_fun f t ∈ open_ball Y d y r.
An exact proof term for the current goal is (SepE2 X (λu : set ⇒ apply_fun f u ∈ open_ball Y d y r) t HtPreB).
We prove the intermediate claim HftY: apply_fun f t ∈ Y.
An exact proof term for the current goal is (Hfun t HtX).
We prove the intermediate claim HftIn: apply_fun f t ∈ V ∩ open_ball Y d y r.
An exact proof term for the current goal is (binintersectI V (open_ball Y d y r) (apply_fun f t) HftV HftB).
An exact proof term for the current goal is (elem_implies_nonempty (V ∩ open_ball Y d y r) (apply_fun f t) HftIn).
We prove the intermediate claim HfxInBig: fx ∈ open_ball Y d y (add_SNo r r).
An exact proof term for the current goal is (closure_open_ball_sub_open_ball_add_radius Y d y r Hm HyY HrR HrPos fx HfxCl).
An exact proof term for the current goal is (SepI X (λu : set ⇒ apply_fun f u ∈ open_ball Y d y (add_SNo r r)) x HxX HfxInBig).
∎