instCommutativeMin_mathlib

Mathlib.Order.Lattice

URI: https://scilib.ai/kg/mathlib#instCommutativeMin_mathlib

English

Let α be a semilattice with meet. Then for all a,b in α, a ⊓ b = b ⊓ a.

Русский

Пусть α — полурешетка с операцией meet. Тогда для любых a,b ∈ α выполняется a ⊓ b = b ⊓ a.

LaTeX

$$$ \forall a,b : \alpha,\ a \wedge b = b \wedge a $$$

Lean4

instance : Std.Commutative (α := α) (· ⊓ ·) :=
  ⟨inf_comm⟩

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

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

Разделы

Аффилиация

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