fst_dual

Mathlib.Order.Interval.Basic

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

English

The first component of the dual of s equals toDual of the second component of s.

Русский

Первая компонента двойственного интервала равна toDual второй компоненты интервала s.

LaTeX

$$$\mathrm{fst}(\mathrm{dual}(s)) = \mathrm{toDual}(\mathrm{snd}(s))$$$

Lean4

@[simp]
theorem fst_dual (s : NonemptyInterval α) : s.dual.fst = toDual s.snd :=
  rfl

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

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

Разделы

Аффилиация

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