snd — Mathlib

English

If f is continuous within s at x and g is continuous within s at x, then 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

@[fun_prop]
theorem snd {f : α → β × γ} {s : Set α} (hf : ContinuousOn f s) : ContinuousOn (fun x => (f x).2) s :=
  continuous_snd.comp_continuousOn hf

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