map_snd_nhds

Mathlib.Topology.Constructions.SumProd

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

← MathLib Explorer

English

The map snd sends nhds to nhds in the second coordinate.

Русский

Отображение snd переводит nhds в nhds по второй координате.

LaTeX

$$$$\mathrm{map}\;\mathrm{Prod.snd}\,(\mathcal N_{(x,y)}) = \mathcal N_y.$$$$

Lean4

@[simp]
theorem map_snd_nhds (x : X × Y) : map Prod.snd (𝓝 x) = 𝓝 x.2 :=
  le_antisymm continuousAt_snd <| (map_snd_nhdsWithin x).symm.trans_le (map_mono inf_le_left)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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