snd' — Mathlib

English

If f: Y → Z is continuous at y, then the map (x, y) ↦ f(y) is continuous at (x, y) for any x.

Русский

Пусть f: Y → Z непрерывна в y. Тогда отображение (x, y) ↦ f(y) непрерывно в (x, y).

LaTeX

$$$\operatorname{ContinuousAt}(f, y) \Rightarrow \operatorname{ContinuousAt}(\lambda p:(X\times Y), f(p_2), (x,y))$$$

Lean4

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

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