snd — Mathlib

English

Let f: X → Y × Z be continuous at x. Then the map x ↦ π2(f(x)) is continuous at x, where π2 is the projection onto Z.

Русский

Пусть f: X → Y × Z непрерывна в точке x. Тогда отображение x ↦ π2(f(x)) непрерывно в x, где π2 — вторая проекция на Z.

LaTeX

$$$\operatorname{ContinuousAt}(f, x) \Rightarrow \operatorname{ContinuousAt}(\pi_2 \circ f, x)$$$

Lean4

/-- Postcomposing `f` with `Prod.snd` is continuous at `x` -/
@[fun_prop]
theorem snd {f : X → Y × Z} {x : X} (hf : ContinuousAt f x) : ContinuousAt (fun x : X => (f x).2) x :=
  continuousAt_snd.comp hf

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