mem_closure_iff — Mathlib

English

In a seminormed group, x ∈ closure(s) iff for all ε>0, there exists b ∈ s with ‖a/b‖ < ε.

Русский

В семинормированной группе x принадлежит замыканию s тогда и только тогда, когда для любого ε>0 найдется b ∈ s такое, что ‖a/b‖ < ε.

LaTeX

$$$ a \in \overline{s} \iff \forall \varepsilon>0, \exists b \in s, \|a/b\| < \varepsilon. $$$

Lean4

@[to_additive]
theorem mem_closure_iff : a ∈ closure s ↔ ∀ ε, 0 < ε → ∃ b ∈ s, ‖a / b‖ < ε := by
  simp [Metric.mem_closure_iff, dist_eq_norm_div]

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