mk_inf_mk

Mathlib.Order.Lattice

URI: https://scilib.ai/kg/mathlib#Prod.mk_inf_mk

English

The infimum on the product is coordinatewise: (a1,b1) ⊓ (a2,b2) = (a1 ⊓ a2, b1 ⊓ b2).

Русский

На произведении инфимум задаётся покоординатно: (a1,b1) ⊓ (a2,b2) = (a1 ⊓ a2, b1 ⊓ b2).

LaTeX

$$$(a_1,b_1)\land (a_2,b_2)=(a_1\land a_2,b_1\land b_2)$$$

Lean4

@[simp]
theorem mk_inf_mk [Min α] [Min β] (a₁ a₂ : α) (b₁ b₂ : β) : (a₁, b₁) ⊓ (a₂, b₂) = (a₁ ⊓ a₂, b₁ ⊓ b₂) :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru