top_mem_iff

Mathlib.Order.Antichain

URI: https://scilib.ai/kg/mathlib#IsAntichain.top_mem_iff

English

If s is an antichain under ≤, then ⊤ ∈ s iff s = {⊤}.

Русский

Если s — антицепь под ≤, то ⊤ принадлежит s тогда и только тогда, когда s = {⊤}.

LaTeX

$$$IsAntichain(\\le) s \\rightarrow (⊤ \\in s \\iff s = \\{⊤\\}).$$$

Lean4

theorem top_mem_iff [OrderTop α] (hs : IsAntichain (· ≤ ·) s) : ⊤ ∈ s ↔ s = {⊤} :=
  isGreatest_top_iff.symm.trans hs.greatest_iff

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

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

Разделы

Аффилиация

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