nhdsSet_diagonal_le_uniformity — Mathlib

English

The diagonal neighborhood filter is bounded above by the supremum of nhds at each point along the diagonal with iSup over x.

Русский

Фильтр окрестностей диагонали ограничен верхней границей по iSup от x вдоль диагонали.

LaTeX

$$$\\mathcal{N}^{\text{set}}(\\Delta α) \\le \\bigvee_{x} 𝓝(x,x) \\le 𝓤 α$$$

Lean4

/-- Entourages are neighborhoods of the diagonal. -/
theorem nhdsSet_diagonal_le_uniformity : 𝓝ˢ (diagonal α) ≤ 𝓤 α :=
  (nhdsSet_diagonal α).trans_le iSup_nhds_le_uniformity

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