swap_inf

Mathlib.Order.Lattice

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

English

The swap operation commutes with pointwise inf: (p ⊓ q).swap = p.swap ⊓ q.swap.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem swap_inf [Min α] [Min β] (p q : α × β) : (p ⊓ q).swap = p.swap ⊓ q.swap :=
  rfl

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

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

Разделы

Аффилиация

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