inf_right_idem

Mathlib.Order.Lattice

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

English

Right idempotence of meet: a ⊓ b ⊓ b = a ⊓ b.

Русский

Правая идемпотентность meet: a ⊓ b ⊓ b = a ⊓ b.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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