snd — Mathlib

English

Precomposing f with Prod.snd is continuous in the sense that the map x ↦ f(x).snd is continuous whenever f is continuous.

Русский

Предобраз через Prod.snd непрерывен: если f непрерывна, то x ↦ f(x).snd непрерывна.

LaTeX

$$$\\operatorname{Continuous}(f) \\Rightarrow \\operatorname{Continuous}(x \\mapsto (f x).snd)$$$

Lean4

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

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