English
If x is not in the domain of f and y ∈ f.val.domain, there exists z ∈ f.val.domain such that z − x lies in a ball around x with radius mk(y − x).
Русский
Если x не принадлежит области определения f, и y ∈ f.val.domain, существует z ∈ f.val.domain, такой что z − x лежит в шаре вокруг x радиуса mk(y − x).
LaTeX
$$$\\exists z\\in f.val.domain,\\; z\\!-\!x\\in B_K(\\operatorname{mk}(y-x)).$$$
Lean4
/-- For `x` not in `f`'s domain, there is an infinite chain of `y` from `f`'s domain
that keeps getting closer to `x` in terms of Archimedean classes. -/
theorem exists_sub_mem_ball [IsOrderedAddMonoid R] [Archimedean R] {x : M} (hx : x ∉ f.val.domain) (y : f.val.domain) :
∃ z : f.val.domain, z.val - x ∈ ball K (mk (y.val - x)) :=
by
have : y.val - x ≠ 0 := by
contrapose! hx
obtain rfl : x = y.val := (sub_eq_zero.mp hx).symm
simp
let c := FiniteArchimedeanClass.mk (y.val - x) this
have hc : mk (y.val - x) = c.val := rfl
contrapose! hx
obtain h := f.eval_eq_truncLT hc hx
obtain ⟨x', hx'⟩ := LinearMap.mem_range.mp (f.prop.truncLT_mem_range y c)
rw [← hx'] at h
contrapose! h
exact f.eval_ne h _
