inf_left_idem

Mathlib.Order.Lattice

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

English

Left idempotence of meet: a ⊓ (a ⊓ b) = a ⊓ b.

Русский

Левый идемпотент meet: a ⊓ (a ⊓ b) = a ⊓ b.

LaTeX

$$$ \forall a,b,\ a \wedge (a \wedge b) = a \wedge b $$$

Lean4

theorem inf_left_idem (a b : α) : a ⊓ (a ⊓ b) = a ⊓ b := by simp

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

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

Разделы

Аффилиация

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