uniformSpace_eq_bot — Mathlib

English

A uniform space is the bottom uniform space if and only if the diagonal idRel belongs to its uniformity.

Русский

Равномерное пространство равно нижнему, если и только если диагональная связность idRel принадлежит его uniformity.

LaTeX

$$u = ⊥ ⇔ idRel ∈ 𝓤[u]$$

Lean4

theorem uniformSpace_eq_bot {u : UniformSpace α} : u = ⊥ ↔ idRel ∈ 𝓤[u] :=
  le_bot_iff.symm.trans le_principal_iff

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