fst_inf

Mathlib.Order.Lattice

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

English

The first projection preserves infimum: (p ⊓ q).fst = p.fst ⊓ q.fst.

Русский

Первая проекция сохраняет инфимум: (p ⊓ q).fst = p.fst ⊓ q.fst.

LaTeX

$$$\text{fst}(p\land q)=\text{fst}(p)\land\text{fst}(q)$$$

Lean4

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

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

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

Разделы

Аффилиация

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