nhds_swap

Mathlib.Topology.Constructions.SumProd

URI: https://scilib.ai/kg/mathlib#nhds_swap

English

The neighborhood of (x,y) is the image under swap of the neighborhood of (y,x).

Русский

Окрестности (x,y) равны образу окрестности (y,x) под отображение swap.

LaTeX

$$$ 𝓝 (x, y) = (𝓝 (y, x)).map Prod.swap $$$

Lean4

theorem nhds_swap (x : X) (y : Y) : 𝓝 (x, y) = (𝓝 (y, x)).map Prod.swap := by
  rw [nhds_prod_eq, Filter.prod_comm, nhds_prod_eq]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru