continuousWithinAt_fst

Mathlib.Topology.ContinuousOn

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

English

For any set s of pairs and any point p, the map Prod.fst is continuous within s at p.

Русский

Для любого множества пар s и любой точки p карта Prod.fst непрерывна внутри s в p.

LaTeX

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

Lean4

theorem continuousWithinAt_fst {s : Set (α × β)} {p : α × β} : ContinuousWithinAt Prod.fst s p :=
  continuous_fst.continuousWithinAt

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

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

Разделы

Аффилиация

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