continuousAt_snd

Mathlib.Topology.Constructions.SumProd

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

English

The map p ↦ p.snd: X × Y → Y is continuous at every point p.

Русский

Отображение p ↦ p.snd из X × Y в Y непрерывно в каждой точке.

LaTeX

$$$\\operatorname{ContinuousAt}(\\operatorname{Prod.snd}, p)$ for all p ∈ X × Y$$

Lean4

theorem continuousAt_snd {p : X × Y} : ContinuousAt Prod.snd p :=
  continuous_snd.continuousAt

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

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

Разделы

Аффилиация

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