isAntichain_and_least_iff — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem isAntichain_and_least_iff : IsAntichain (· ≤ ·) s ∧ IsLeast 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, isLeast_singleton⟩⟩

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