iSup_nhds_le_uniformity — Mathlib

English

Entourages absorb the diagonal: the neighborhood filter of the diagonal is contained in the uniformity.

Русский

Окружности окружают диагональ: фильтр окрестностей диагонали включён в униформность.

LaTeX

$$$\\mathcal{N}ˢ(\\mathrm{diagonal}(α)) \\le 𝓤 α$$$

Lean4

/-- Entourages are neighborhoods of the diagonal. -/
theorem iSup_nhds_le_uniformity : ⨆ x : α, 𝓝 (x, x) ≤ 𝓤 α :=
  iSup_le nhds_le_uniformity

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