ext — Mathlib

English

Two uniform spaces are equal if and only if their uniformities are equal.

Русский

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

LaTeX

$$$\\forall {u_1 u_2 : UniformSpace\\alpha},\\; u_1.uniformity = u_2.uniformity \\Rightarrow u_1 = u_2$$$

Lean4

@[ext (iff := false)]
protected theorem ext {u₁ u₂ : UniformSpace α} (h : 𝓤[u₁] = 𝓤[u₂]) : u₁ = u₂ :=
  by
  have : u₁.toTopologicalSpace = u₂.toTopologicalSpace :=
    TopologicalSpace.ext_nhds fun x ↦
      by
      rw [u₁.nhds_eq_comap_uniformity, u₂.nhds_eq_comap_uniformity]
      exact congr_arg (comap _) h
  cases u₁; cases u₂; congr

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