snd_sub

Mathlib.Algebra.Order.Interval.Basic

URI: https://scilib.ai/kg/mathlib#NonemptyInterval.snd_sub

English

The right endpoint of s - t equals s.snd - t.fst.

Русский

Правая граница (s - t) равна s.snd - t.fst.

LaTeX

$$$\mathrm{snd}(s - t) = \mathrm{snd}(s) - \mathrm{fst}(t)$$$

Lean4

@[simp]
theorem snd_sub : (s - t).snd = s.snd - t.fst :=
  rfl

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

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

Разделы

Аффилиация

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