inf_assoc

Mathlib.Algebra.Ring.BooleanRing

URI: https://scilib.ai/kg/mathlib#BooleanRing.inf_assoc

English

Infimum is associative: (a ∧ b) ∧ c = a ∧ (b ∧ c).

Русский

Наименьшее (пересечение) ассоциативно: (a ∧ b) ∧ c = a ∧ (b ∧ c).

LaTeX

$$$(a \land b) \land c = a \land (b \land c)$$$

Lean4

theorem inf_assoc (a b c : α) : a ⊓ b ⊓ c = a ⊓ (b ⊓ c) :=
  by
  dsimp only [(· ⊓ ·)]
  ring

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

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

Разделы

Аффилиация

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