fst''

Mathlib.Topology.Constructions.SumProd

URI: https://scilib.ai/kg/mathlib#ContinuousAt.fst''

← MathLib Explorer

English

The map x ↦ x.fst from X × Y to X is continuous.

Русский

Отображение x ↦ x.fst из X × Y в X непрерывно.

LaTeX

$$$\\operatorname{Continuous}(\\operatorname{Prod.fst})$$$

Lean4

/-- Precomposing `f` with `Prod.fst` is continuous at `x : X × Y` -/
theorem fst'' {f : X → Z} {x : X × Y} (hf : ContinuousAt f x.fst) : ContinuousAt (fun x : X × Y => f x.fst) x :=
  hf.comp continuousAt_fst

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

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

Разделы

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

Аффилиация

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