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 _⟩