instSubInterval

Mathlib.Algebra.Order.Interval.Basic

URI: https://scilib.ai/kg/mathlib#instSubInterval

English

Subtraction on intervals is defined componentwise by subtracting endpoints: s - t = (s.fst - t.snd, s.snd - t.fst).

Русский

Вычитание интервалов определено по компонентам: s - t = (s.fst - t.snd, s.snd - t.fst).

LaTeX

$$$s - t = (s.fst - t.snd,\; s.snd - t.fst),$$$

Lean4

instance : Sub (Interval α) :=
  ⟨WithBot.map₂ Sub.sub⟩

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

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

Разделы

Аффилиация

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