coe_inf

Mathlib.Order.Sublocale

URI: https://scilib.ai/kg/mathlib#Sublocale.coe_inf

English

The underlying value preserves binary infimum: (a ⊓ b).val = a.val ⊓ b.val.

Русский

Прообраз двойного meet сохраняет инфимум: (a ⊓ b).val = a.val ⊓ b.val.

LaTeX

$$$(a \wedge b).\text{val} = a.\text{val} \wedge b.\text{val}$$$

Lean4

@[simp, norm_cast]
theorem coe_inf (a b : S) : (a ⊓ b).val = ↑a ⊓ ↑b :=
  rfl

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

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

Разделы

Аффилиация

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