orderIsoPair_one

Mathlib.Order.Fin.Finset

URI: https://scilib.ai/kg/mathlib#Fin.orderIsoPair_one

English

The image of 1 under the pair isomorphism is b.

Русский

Образ 1 при этом изоморфизме равен b.

LaTeX

$$$(orderIsoPair\ a\ b\ hab)(1)=b.$$$

Lean4

@[simp]
theorem orderIsoPair_one : orderIsoPair a b hab 1 = b :=
  rfl

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

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

Разделы

Аффилиация

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