snd_dual

Mathlib.Order.Interval.Basic

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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