mem_uniformity_dist — Mathlib

English

A set s ⊆ α×α is in the uniformity if and only if there exists ε > 0 such that dist(a,b) < ε implies (a,b) ∈ s.

Русский

Множество s ⊆ α×α принадлежит униформности тогда и только тогда, существует ε>0 такое, что dist(a,b) < ε ⇒ (a,b) ∈ s.

LaTeX

$$$$ s \in \mathcal{U}(\alpha) \iff \exists \varepsilon > 0, \forall a,b \in \alpha, \operatorname{dist}(a,b) < \varepsilon \Rightarrow (a,b) \in s. $$$$

Lean4

theorem mem_uniformity_dist {s : Set (α × α)} : s ∈ 𝓤 α ↔ ∃ ε > 0, ∀ ⦃a b : α⦄, dist a b < ε → (a, b) ∈ s :=
  uniformity_basis_dist.mem_uniformity_iff

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