comp₂_of_eq — Mathlib

English

If f is continuous at y, g x and h x converge to y with e: (g x, h x) = y, then f (g x, h x) is continuous at x.

Русский

Если f непрерывна в y, а (g x, h x) сходится к y по отношению к x и e: (g x, h x) = y, то f(g x, h x) непрерывна в x.

LaTeX

$$$ (ContinuousAt f y) \\land (ContinuousAt g x) \\land (ContinuousAt h x) \\land e : (g x, h x) = y \\Rightarrow ContinuousAt (\\\\lambda x. f (g x, h x)) x $$$

Lean4

theorem comp₂_of_eq {f : Y × Z → W} {g : X → Y} {h : X → Z} {x : X} {y : Y × Z} (hf : ContinuousAt f y)
    (hg : ContinuousAt g x) (hh : ContinuousAt h x) (e : (g x, h x) = y) : ContinuousAt (fun x ↦ f (g x, h x)) x :=
  by
  rw [← e] at hf
  exact hf.comp₂ hg hh

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