dense_iff_iUnion_ball — Mathlib

English

A subset s is dense in α iff every nonempty open interval (ball) around any point intersects s.

Русский

Подмножество s плотное в α тогда и только тогда, когда каждый открытый интервал (окружность) вокруг любой точки пересекается с s.

LaTeX

$$$\text{Dense } s \iff \forall x,\forall r>0,\,(\operatorname{ball}(x,r) \cap s)\neq \emptyset$$$

Lean4

theorem dense_iff_iUnion_ball (s : Set α) : Dense s ↔ ∀ r > 0, ⋃ c ∈ s, ball c r = univ := by
  simp_rw [eq_univ_iff_forall, mem_iUnion, exists_prop, mem_ball, Dense, mem_closure_iff, forall_comm (α := α)]

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