snd' — Mathlib

English

If f is continuous at x in X, then the map (x,y) ↦ f(x) restricted to the first coordinate is continuous at (x,y).

Русский

Если f непрерывна в точке x, то отображение (x,y) ↦ f(x) непрерывно в точке (x,y) по первому координату.

LaTeX

$$$\\text{ContinuousAt}(f, x) \\Rightarrow \\text{ContinuousAt}(\\lambda p. f(p.1), p) \\text{ for } p=(x,y)$$$

Lean4

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

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