sup_eq_iff_inf_eq

Mathlib.Order.Lattice

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

English

In a lattice, a ∨ b = b iff a ∧ b = a.

Русский

В решётке a ∨ b = b тогда и только тогда, когда a ∧ b = a.

LaTeX

$$$ a \vee b = b \iff a \wedge b = a$$$

Lean4

theorem sup_eq_iff_inf_eq : a ⊔ b = b ↔ a ⊓ b = a := by rw [sup_eq_right, ← inf_eq_left]

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

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

Разделы

Аффилиация

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