fst — Mathlib

English

For any p = (x,y) in X × Y, the map that sends a neighborhood to its first coordinate is continuous at p.

Русский

Для любой точки p = (x,y) в X × Y отображение соседствующих точек в первую координату непрерывно в p.

LaTeX

$$$\\operatorname{ContinuousAt}(\\operatorname{Prod.fst}, p)$$$

Lean4

/-- Postcomposing `f` with `Prod.fst` is continuous -/
@[fun_prop]
theorem fst {f : X → Y × Z} (hf : Continuous f) : Continuous fun x : X => (f x).1 :=
  continuous_fst.comp hf

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