instSemilatticeInf — Mathlib

English

If α and β have semilattice infimum, then α × β has SemilatticeInf defined coordinatewise: (a,b) ⊓ (c,d) = (a ⊓ c, b ⊓ d).

Русский

Если α и β имеют Inf, то α×β имеет Inf по координатам: (a,b) ⊓ (c,d) = (a ⊓ c, b ⊓ d).

LaTeX

$$$ (a,b) \land (c,d) = (a \land c, b \land d) $$$

Lean4

instance instSemilatticeInf [SemilatticeInf α] [SemilatticeInf β] : SemilatticeInf (α × β)
    where
  inf a b := ⟨a.1 ⊓ b.1, a.2 ⊓ b.2⟩
  le_inf _ _ _ h₁ h₂ := ⟨le_inf h₁.1 h₂.1, le_inf h₁.2 h₂.2⟩
  inf_le_left _ _ := ⟨inf_le_left, inf_le_left⟩
  inf_le_right _ _ := ⟨inf_le_right, inf_le_right⟩

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