swap_sup

Mathlib.Order.Lattice

URI: https://scilib.ai/kg/mathlib#Prod.swap_sup

English

The swap operation commutes with pointwise sup: (p ⊔ q).swap = p.swap ⊔ q.swap.

Русский

Операция разворота (swap) commuting with pointwise sup: (p ⊔ q).swap = p.swap ⊔ q.swap.

LaTeX

$$$ (p\lor q).swap = p.swap \lor q.swap $$$

Lean4

@[simp]
theorem swap_sup [Max α] [Max β] (p q : α × β) : (p ⊔ q).swap = p.swap ⊔ q.swap :=
  rfl

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

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

Разделы

Аффилиация

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