minimal_mem_iff — Mathlib

English

Let (A, ≤) be a preorder and S ⊆ A an antichain with respect to ≤. Then for every a in A, a is a minimal element of S with respect to ≤ if and only if a ∈ S.

Русский

Пусть (A, ≤) — предупорядоченное множество и S ⊆ A антицепь относительно ≤. Тогда для каждого элемента a ∈ A выполняется: a — минимальный элемент S по отношению к ≤ тогда и только тогда, когда a ∈ S.

LaTeX

$$$\\operatorname{IsAntichain}(\\le, s) \\Rightarrow \\forall a, \\operatorname{Min}_{\\le}(a; s) \\iff a \\in s$$$

Lean4

theorem minimal_mem_iff (hs : IsAntichain (· ≤ ·) s) : Minimal (· ∈ s) a ↔ a ∈ s :=
  ⟨fun h ↦ h.prop, fun h ↦ ⟨h, fun _ hys hyx ↦ (hs.eq hys h hyx).symm.le⟩⟩

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