top — Mathlib

English

The top (trivial) uniformity gives an ultra-uniform structure.

Русский

Верхняя (тождественно-нулевая) равномерность задает ультра-структуру.

LaTeX

$$$IsUltraUniformity\big(X\big)\;\text{for top uniformity}$$$

Lean4

theorem top : @IsUltraUniformity X (⊤ : UniformSpace X) :=
  by
  letI : UniformSpace X := ⊤
  have := Filter.hasBasis_top (α := (X × X))
  rw [← top_uniformity] at this
  apply mk_of_hasBasis this
  · simpa using isSymmetricRel_univ
  · simpa using isTransitiveRel_univ

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