isAntichain_and_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 isAntichain_and_greatest_iff : IsAntichain (· ≤ ·) s ∧ IsGreatest s a ↔ s = { a } :=
  ⟨fun h => eq_singleton_iff_unique_mem.2 ⟨h.2.1, fun _ hb => h.1.eq hb h.2.1 (h.2.2 hb)⟩,
    by
    rintro rfl
    exact ⟨IsAntichain.singleton, isGreatest_singleton⟩⟩

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