antichain_iff

Mathlib.Order.Antichain

URI: https://scilib.ai/kg/mathlib#IsLeast.antichain_iff

English

If hs is IsLeast s a, then IsAntichain (≤) s ↔ s = {a}.

Русский

Если hs : IsLeast s a, тогда IsAntichain (≤) s ⇔ s = {a}.

LaTeX

$$$IsLeast s a \\rightarrow (IsAntichain(\\le) s \\iff s = \\{a\\}).$$$

Lean4

theorem antichain_iff (hs : IsLeast s a) : IsAntichain (· ≤ ·) s ↔ s = { a } :=
  (and_iff_left hs).symm.trans isAntichain_and_least_iff

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

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

Разделы

Аффилиация

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