instMax_mathlib — Mathlib

English

If α and β have binary maximums, then the product α × β has a maximum defined coordinatewise: (a1,b1) ⊔ (a2,b2) = (a1 ⊔ a2, b1 ⊔ b2).

Русский

Если у α и β есть максимум, то произведение α × β имеет максимум, задаваемый по координатам: (a1,b1) ⊔ (a2,b2) = (a1 ⊔ a2, b1 ⊔ b2).

LaTeX

$$$\forall a_1,a_2:\ (a_1,b_1) \lor (a_2,b_2) = (a_1 \lor a_2, b_1 \lor b_2)$$$

Lean4

instance [Max α] [Max β] : Max (α × β) :=
  ⟨fun p q => ⟨p.1 ⊔ q.1, p.2 ⊔ q.2⟩⟩

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