snd — Mathlib

English

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

Русский

Проекция на β сохраняет операции объединения и пересечения.

LaTeX

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

Lean4

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

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