vsub — Mathlib

English

For families of points in a torsor, the subtraction map is continuous; i.e., the operation (f,g) ↦ f -ᵥ g is continuous if f and g are continuous.

Русский

Для функций в торсоре операция вычитания непрерывна: f(x) -ᵥ g(x) непрерывна если f и g непрерывны.

LaTeX

$$$\text{Continuous}(f) \land \text{Continuous}(g) \Rightarrow \text{Continuous}(x \mapsto f(x) -\!ᵥ g(x)).$$$

Lean4

@[fun_prop]
theorem vsub {f g : α → P} (hf : Continuous f) (hg : Continuous g) : Continuous (fun x ↦ f x -ᵥ g x) :=
  continuous_vsub.comp₂ hf hg

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