sub

Mathlib.Analysis.Real.Hyperreal

URI: https://scilib.ai/kg/mathlib#Hyperreal.IsSt.sub

English

If x IsSt r and y IsSt s, then x − y is IsSt (r − s).

Русский

Если x IsSt r и y IsSt s, то x − y IsSt (r − s).

LaTeX

$$$\forall {x y} {r s}, \; x.IsSt r \to y.IsSt s \to \mathrm{IsSt}(x - y, r - s)$$$

Lean4

theorem sub {x y : ℝ*} {r s : ℝ} (hxr : IsSt x r) (hys : IsSt y s) : IsSt (x - y) (r - s) :=
  hxr.map₂ hys continuous_sub.continuousAt

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

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

Разделы

Аффилиация

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