vsub — Mathlib

English

If f and g are continuous within a set s at x, then f -ᵥ g is continuous within s at x.

Русский

Если f и g непрерывны внутри множества s в точке x, то f -ᵥ g непрерывна внутри s в x.

LaTeX

$$$\text{ContinuousWithinAt}(f,s,x) \land \text{ContinuousWithinAt}(g,s,x) \Rightarrow \text{ContinuousWithinAt}(f -ᵥ g,s,x).$$$

Lean4

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

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