ext_iff — Mathlib

English

Two UniformSpace α are equal if and only if they have the same membership in the uniformity filter for all sets.

Русский

Два UniformSpace α равны тогда и только тогда, когда для всех множеств выполняется равенство принадлежности в равномерности.

LaTeX

$$$\\forall {u_1 u_2 : UniformSpace \\alpha},\\; u_1 = u_2 \\iff \\forall s, s \\in 𝓤[ u_1 ] \\iff s \\in 𝓤[ u_2 ]$$$

Lean4

protected theorem ext_iff {u₁ u₂ : UniformSpace α} : u₁ = u₂ ↔ ∀ s, s ∈ 𝓤[u₁] ↔ s ∈ 𝓤[u₂] :=
  ⟨fun h _ => h ▸ Iff.rfl, fun h => by ext; exact h _⟩

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