greatest_iff — Mathlib

English

If s is an antichain under ≤ and a is its greatest element, then s = {a}. Conversely, if s = {a}, then s is an antichain and a is its greatest element.

Русский

Если s — антицепь под ≤ и a — её наибольший элемент, то s = {a}. Обратно, если s = {a}, то s — антицепь и a — наибольший элемент.

LaTeX

$$$IsAntichain(\\le)\\ s \\land IsGreatest(s,a) \\iff s = \\{a\\}. $$$

Lean4

theorem greatest_iff (hs : IsAntichain (· ≤ ·) s) : IsGreatest s a ↔ s = { a } :=
  (and_iff_right hs).symm.trans isAntichain_and_greatest_iff

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