English
Let t be an antichain with respect to ≤. If every minimal element of s is in t and for every a ∈ t there exists b with a ≤ b and b is minimal in s, then the set of minimal elements of s equals t.
Русский
Пусть t является антицепочкой относительно ≤. Если каждый минимальный элемент s принадлежит t, и для каждого a ∈ t существует b с a ≤ b и b минимальный элемент s, тогда множество минимальных элементов s равно t.
LaTeX
$$$\\operatorname{IsAntichain}(\\le, t) \\rightarrow (\\forall x, \\operatorname{Minimal}(x; s) \\rightarrow x \\in t) \\rightarrow (\\forall a \\in t, \\exists b: a \\le b \\land \\operatorname{Minimal}(b; s)) \\Rightarrow \\{x \\mid \\operatorname{Minimal}(x; s)\\} = t$$$
Lean4
/-- If `t` is an antichain shadowed by and including the set of minimal elements of `s`,
then `t` *is* the set of minimal elements of `s`. -/
theorem eq_setOf_minimal (ht : IsAntichain (· ≤ ·) t) (h : ∀ x, Minimal (· ∈ s) x → x ∈ t)
(hs : ∀ a ∈ t, ∃ b, a ≤ b ∧ Minimal (· ∈ s) b) : {x | Minimal (· ∈ s) x} = t :=
ht.to_dual.eq_setOf_maximal h hs
