snd'' — Mathlib

English

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

Русский

Если f: Y → Z непрерывна в x. snd, тогда отображение (x, y) ↦ f(y) непрерывно в (x, y).

LaTeX

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

Lean4

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

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