nhdsSet_diagonal — Mathlib

English

The set-neighborhood of the diagonal in X×X equals the supremum of neighborhoods at each diagonal point: 𝓝ˢ(diagonal X) = ⨆ x, 𝓝(x,x).

Русский

Окружность по множеству диагонали в X×X равна наибольшему объединению окрестностей по каждой точке диагонали: 𝓝ˢ(diagonal X) = ⨆ x, 𝓝(x,x).

LaTeX

$$$nhdsSet(\\mathrm{diagonal}\,X) = \\bigvee_{x\\in X} nhds(x,x)$$$

Lean4

theorem nhdsSet_diagonal (X) [TopologicalSpace (X × X)] : 𝓝ˢ (diagonal X) = ⨆ (x : X), 𝓝 (x, x) :=
  by
  rw [nhdsSet, ← range_diag, ← range_comp]
  rfl

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