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⟩⟩