inf_eq_top_iff

Mathlib.Order.BoundedOrder.Lattice

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

English

In a lattice with top, a ⊓ b = ⊤ iff a = ⊤ ∧ b = ⊤.

Русский

В решётке с верхней границей a ⊓ b = ⊤ тогда и только тогда, когда a = ⊤ и b = ⊤.

LaTeX

$$$a \\;⊓\\; b = \\top \\;\\iff\\; a = \\top \\land b = \\top$$$

Lean4

@[simp]
theorem inf_eq_top_iff : a ⊓ b = ⊤ ↔ a = ⊤ ∧ b = ⊤ :=
  @sup_eq_bot_iff αᵒᵈ _ _ _ _

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

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

Разделы

Аффилиация

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