pair_succ

Mathlib.Order.OmegaCompletePartialOrder

URI: https://scilib.ai/kg/mathlib#OmegaCompletePartialOrder.Chain.pair_succ

English

For the pair construction, the value at index n+1 is always the second element b.

Русский

Для пары, на индексе n+1 значение равно второму элементу b.

LaTeX

$$$$ (\text{pair } a b hab)(n+1) = b. $$$$

Lean4

@[simp]
theorem pair_succ (a b : α) (hab) (n : ℕ) : pair a b hab (n + 1) = b :=
  rfl

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

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

Разделы

Аффилиация

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