exists_dist_lt — Mathlib

English

Density implies arbitrarily close points from the dense set.

Русский

Плотность означает наличие точек из плотного множества, близких к заданной точке.

LaTeX

$$Dense s → ∀ x, ∀ ε>0, ∃ y ∈ s, dist x y < ε$$

Lean4

theorem _root_.Dense.exists_dist_lt {s : Set α} (hs : Dense s) (x : α) {ε : ℝ} (hε : 0 < ε) : ∃ y ∈ s, dist x y < ε :=
  by
  have : (ball x ε).Nonempty := by simp [hε]
  simpa only [mem_ball'] using hs.exists_mem_open isOpen_ball this

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