exists_ball_subset_ball — Mathlib

English

If y is in ball x ε, there exists ε' > 0 such that ball around y with radius ε' is contained in ball around x with radius ε.

Русский

Если y ∈ B(x, ε), существует ε' > 0, такое что B(y, ε') ⊆ B(x, ε).

LaTeX

$$$ y \in B(x, ε) \Rightarrow \exists ε' > 0, B(y, ε') \subseteq B(x, ε) $$$

Lean4

theorem exists_ball_subset_ball (h : y ∈ ball x ε) : ∃ ε' > 0, ball y ε' ⊆ ball x ε :=
  ⟨_, sub_pos.2 h, ball_subset <| by rw [sub_sub_self]⟩

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