enatSub — Mathlib

English

If f,g: X → ENat are continuous at x and for all x the not-both-∞ condition holds, then x ↦ f(x) - g(x) is continuous at x.

Русский

Если f,g: X → ENat непрерывны в точке x и выполняется условие не обе бесконечны, то x ↦ f(x) - g(x) непрерывна в x.

LaTeX

$$$$\\text{ContinuousAt}(f - g, x)$$ при условии $f(x) ≠ ∞ ∨ g(x) ≠ ∞$ и $f,g$ непрерывны в x.$$

Lean4

nonrec theorem enatSub (hf : ContinuousAt f x) (hg : ContinuousAt g x) (h : f x ≠ ⊤ ∨ g x ≠ ⊤) :
    ContinuousAt (fun x ↦ f x - g x) x :=
  hf.enatSub hg h

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