fst

Mathlib.Topology.ContinuousOn

URI: https://scilib.ai/kg/mathlib#ContinuousWithinAt.fst

← MathLib Explorer

English

For any f into a product, fst is continuous within at any point.

Русский

Для любого отображения в произведение fst непрерывна внутри.

LaTeX

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

Lean4

theorem fst {f : α → β × γ} {s : Set α} {a : α} (h : ContinuousWithinAt f s a) :
    ContinuousWithinAt (fun x => (f x).fst) s a :=
  continuousAt_fst.comp_continuousWithinAt h

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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