fst

Mathlib.Topology.ContinuousOn

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

← MathLib Explorer

English

First projection is continuous on set of pairs.

Русский

Первая проекция непрерывна на множестве пар.

LaTeX

$$$\text{ContinuousOn } Prod.fst s$$$

Lean4

@[fun_prop]
theorem fst {f : α → β × γ} {s : Set α} (hf : ContinuousOn f s) : ContinuousOn (fun x => (f x).1) s :=
  continuous_fst.comp_continuousOn hf

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

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

Разделы

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

Аффилиация

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