snd — Mathlib

English

If both f and g are continuous within s at x, then the map x ↦ (f x, g x) is continuous within s at x.

Русский

Если f и g непрерывны внутри s в x, то карта x ↦ (f x, g x) непрерывна внутри s в x.

LaTeX

$$$\text{ ContinuousWithinAt } f s x \to \text{ ContinuousWithinAt } g s x \to \text{ ContinuousWithinAt } (\lambda x. (f x, g x)) s x$$$

Lean4

theorem snd {f : α → β × γ} {s : Set α} {a : α} (h : ContinuousWithinAt f s a) :
    ContinuousWithinAt (fun x => (f x).snd) s a :=
  continuousAt_snd.comp_continuousWithinAt h

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