instMin_mathlib — Mathlib

English

If α and β have binary minimums, then the product α × β has a minimum 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) \land (a_2,b_2) = (a_1 \land a_2, b_1 \land b_2)$$$

Lean4

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

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