enatSub — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

nonrec theorem enatSub (hf : ContinuousOn f s) (hg : ContinuousOn g s) (h : ∀ x ∈ s, f x ≠ ⊤ ∨ g x ≠ ⊤) :
    ContinuousOn (fun x ↦ f x - g x) s := fun x hx ↦ (hf x hx).enatSub (hg x hx) (h x hx)

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