vsub

Mathlib.Topology.Algebra.Group.AddTorsor

URI: https://scilib.ai/kg/mathlib#ContinuousAt.vsub

← MathLib Explorer

English

If f and g are continuous at a point x, then f -ᵥ g is continuous at x.

Русский

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

LaTeX

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

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru