continuousWithinAt_snd

Mathlib.Topology.ContinuousOn

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

English

If f maps into a product, then snd is continuous within at f.

Русский

Если f отображает в произведение, то snd непрерывна внутри.

LaTeX

$$$\text{ContinuousWithinAt } Prod.snd s p$$$

Lean4

theorem continuousWithinAt_snd {s : Set (α × β)} {p : α × β} : ContinuousWithinAt Prod.snd s p :=
  continuous_snd.continuousWithinAt

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

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

Разделы

Аффилиация

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