fst — Mathlib

English

The natural projection from α × β to α preserves sup and inf; i.e., fst((a,b) ∨ (a',b')) = a ∨ a' and fst((a,b) ∧ (a',b')) = a ∧ a'.

Русский

Естественная проекция из α × β на α сохраняет операции объединения и пересечения: fst((a,b) ∨ (a',b')) = a ∨ a', fst((a,b) ∧ (a',b')) = a ∧ a'.

LaTeX

$$$\mathrm{fst}((a,b) \vee (a',b')) = a \vee a', \; \mathrm{fst}((a,b) \wedge (a',b')) = a \wedge a'.$$$

Lean4

/-- Natural projection homomorphism from `α × β` to `α`. -/
def fst : LatticeHom (α × β) α where
  toFun := Prod.fst
  map_sup' _ _ := rfl
  map_inf' _ _ := rfl

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