enatSub — Mathlib

English

If f,g: X → ENat are continuous within a set s at x, and for all x ∈ s we have f(x) ≠ ∞ or g(x) ≠ ∞, then x ↦ f(x) - g(x) is continuous within s at x.

Русский

Если f,g: X → ENat непрерывны внутри множества s в точке x, и для всех x ∈ s выполняется f(x) ≠ ∞ или g(x) ≠ ∞, то x ↦ f(x) - g(x) непрерывна внутри s в x.

LaTeX

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

Lean4

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

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