continuous_swap

Mathlib.Topology.Constructions.SumProd

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

English

If px holds near x and py holds near y, then both hold near (x,y) in nhds (x,y).

Русский

Если px верно близко к x и py близко к y, то оба верны близко к (x,y) в nhds (x,y).

LaTeX

$$prod_inl_nhds y ∧ prod_inr_nhds x ⇒ nhds (x,y) contains (px ∈ first, py ∈ second)$$

Lean4

theorem continuous_swap : Continuous (Prod.swap : X × Y → Y × X) :=
  continuous_snd.prodMk continuous_fst

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

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

Разделы

Аффилиация

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