comp_of_eq — Mathlib

English

If g is continuous at y, f is continuous at x, and f(x) = y, then ContinuousAt(g ∘ f) at x.

Русский

Если g непрерывна в y, f непрерывна в x, и f(x) = y, то g ∘ f непрерывна в x.

LaTeX

$$$\\mathrm{ContinuousAt}(g, y) \\rightarrow \\mathrm{ContinuousAt}(f, x) \\rightarrow f(x) = y \\rightarrow \\mathrm{ContinuousAt}(g \\circ f, x)$$$

Lean4

/-- See note [comp_of_eq lemmas] -/
theorem comp_of_eq {g : Y → Z} (hg : ContinuousAt g y) (hf : ContinuousAt f x) (hy : f x = y) :
    ContinuousAt (g ∘ f) x := by subst hy; exact hg.comp hf

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