exists_lt_mem_ball_of_mem_ball — Mathlib

English

If x ∈ ball y with radius ε, then there exists ε' < ε such that x ∈ ball y ε'.

Русский

Если x ∈ ball(y,ε), то существует ε' < ε такое, что x ∈ ball(y,ε').

LaTeX

$$$ x \in \mathrm{ball}(y,\varepsilon) \Rightarrow \exists \varepsilon' < \varepsilon, x \in \mathrm{ball}(y,\varepsilon') $$$

Lean4

/-- If a point belongs to an open ball, then there is a strictly smaller radius whose ball also
contains it.

See also `exists_lt_subset_ball`. -/
theorem exists_lt_mem_ball_of_mem_ball (h : x ∈ ball y ε) : ∃ ε' < ε, x ∈ ball y ε' :=
  by
  simp only [mem_ball] at h ⊢
  exact ⟨(dist x y + ε) / 2, by linarith, by linarith⟩

Похожие утверждения