le_def — Mathlib

English

The uniformity of the bottom uniform space equals the principal filter on the identity relation: 𝓤[(⊥)].

Русский

Униформность нижнего пространства равна принципиальному фильтру по тождественной relation: 𝓤[(⊥)].

LaTeX

$$$𝓤[(⊥ : UniformSpace α)] = 𝓟 \mathrm{idRel}$$$

Lean4

protected theorem le_def {u₁ u₂ : UniformSpace α} : u₁ ≤ u₂ ↔ 𝓤[u₁] ≤ 𝓤[u₂] :=
  Iff.rfl

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