comp₂_continuousWithinAt — Mathlib

English

If f is continuous at the point (g x, h x), and g,h are continuous within s at x, then f(g x, h x) is continuous within s at x.

Русский

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

LaTeX

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

Lean4

theorem comp₂_continuousWithinAt {f : β × γ → δ} {g : α → β} {h : α → γ} {x : α} {s : Set α}
    (hf : ContinuousAt f (g x, h x)) (hg : ContinuousWithinAt g s x) (hh : ContinuousWithinAt h s x) :
    ContinuousWithinAt (fun x ↦ f (g x, h x)) s x :=
  ContinuousAt.comp_continuousWithinAt hf (hg.prodMk_nhds hh)

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