instSemilatticeSup — Mathlib

English

If α and β have semilattice structures with ⊔, then α × β has a SemilatticeSup defined by (a,b) ⊔ (c,d) = (a ⊔ c, b ⊔ d).

Русский

Если у α и β есть полузамкнутые структуры с ⊔, то у α×β есть SemilatticeSup: (a,b) ⊔ (c,d) = (a ⊔ c, b ⊔ d).

LaTeX

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

Lean4

instance instSemilatticeSup [SemilatticeSup α] [SemilatticeSup β] : SemilatticeSup (α × β)
    where
  sup a b := ⟨a.1 ⊔ b.1, a.2 ⊔ b.2⟩
  sup_le _ _ _ h₁ h₂ := ⟨sup_le h₁.1 h₂.1, sup_le h₁.2 h₂.2⟩
  le_sup_left _ _ := ⟨le_sup_left, le_sup_left⟩
  le_sup_right _ _ := ⟨le_sup_right, le_sup_right⟩

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