vsub — Mathlib

English

If f and g are continuous on a set, then the map x ↦ f(x) -ᵥ g(x) is continuous on that set.

Русский

Если функции f и g непрерывны на множестве, то x ↦ f(x) -ᵥ g(x) непрерывна на этом множестве.

LaTeX

$$$\forall x\, (x \in s) : \text{ContinuousOn}(f,g,s) \Rightarrow \text{ContinuousOn}(x \mapsto f(x) -ᵥ g(x), s).$$$

Lean4

@[fun_prop]
theorem vsub {f g : α → P} {s : Set α} (hf : ContinuousOn f s) (hg : ContinuousOn g s) :
    ContinuousOn (fun x ↦ f x -ᵥ g x) s := fun x hx ↦ (hf x hx).vsub (hg x hx)

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