egauge_eq_zero_iff — Mathlib

English

egauge s x = 0 iff frequently near 0 one can find c with x ∈ c·s.

Русский

egauge s x = 0 эквивалентно тому, что почти при 0 существует c с x ∈ c·s.

LaTeX

$$$\mathrm{egauge}_{\mathbb{K}}(s,x) = 0 \iff \text{Frequently } c \to 0 : x \in c\cdot s$$$

Lean4

theorem egauge_eq_zero_iff : egauge 𝕜 s x = 0 ↔ ∃ᶠ c : 𝕜 in 𝓝 0, x ∈ c • s :=
  by
  refine (iInf₂_eq_bot _).trans ?_
  rw [(nhds_basis_uniformity uniformity_basis_edist).frequently_iff]
  simp [and_comm]

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