bot — Mathlib

English

The bottom (discrete) uniformity is ultra-uniform when X carries discrete uniformity.

Русский

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

LaTeX

$$$IsUltraUniformity\big(X\big)$$$

Lean4

instance bot [UniformSpace X] [DiscreteUniformity X] : IsUltraUniformity X :=
  by
  have := Filter.hasBasis_principal (idRel (α := X))
  rw [← DiscreteUniformity.eq_principal_idRel] at this
  apply mk_of_hasBasis this
  · simpa using isSymmetricRel_idRel
  · simpa using isTransitiveRel_idRel

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