enatSub — Mathlib

English

If f,g: X → ENat are continuous and for all x, f(x) ≠ ∞ or g(x) ≠ ∞, then x ↦ f(x) - g(x) is continuous on X.

Русский

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

LaTeX

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

Lean4

nonrec theorem enatSub (hf : Continuous f) (hg : Continuous g) (h : ∀ x, f x ≠ ⊤ ∨ g x ≠ ⊤) :
    Continuous (fun x ↦ f x - g x) :=
  continuous_iff_continuousAt.2 fun x ↦ hf.continuousAt.enatSub hg.continuousAt (h x)

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