prod_inr_nhds

Mathlib.Topology.Constructions.SumProd

URI: https://scilib.ai/kg/mathlib#Filter.Eventually.prod_inr_nhds

English

For any fixed y, the map x ↦ (x, y) is continuous.

Русский

Для фиксированного y отображение x ↦ (x, y) непрерывно.

LaTeX

$$Continuous (\lambda x, (x, y))$$

Lean4

theorem prod_inr_nhds {p : Y → Prop} {y : Y} (h : ∀ᶠ x in 𝓝 y, p x) (x : X) : ∀ᶠ x in 𝓝 (x, y), p (x : X × Y).2 :=
  continuousAt_snd h

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

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

Разделы

Аффилиация

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