English
Let t be an antichain with respect to ≤. Suppose s is a subset of the ambient set and every x ∈ t which is a maximal element of s lies in t, and every a ∈ t is above some element b that is maximal in s. Then the set of maximal elements of s coincides with t.
Русский
Пусть t является антицепочкой относительно ≤. Предположим, что ∀ x, если x максимальный элемент s, то x ∈ t, и ∀ a ∈ t существует b с b ≤ a и b максимальный элемент s. Тогда множество максимальных элементов s равно t.
LaTeX
$$$\\operatorname{IsAntichain}(\\le, t) \\rightarrow (\\forall x, \\operatorname{Maximal}(x; s) \\rightarrow x \\in t) \\rightarrow (\\forall a \\in t, \\exists b: b \\le a \\land \\operatorname{Maximal}(b; s)) \\Rightarrow \\{x \\mid \\operatorname{Maximal}(x; s)\\} = t$$$
Lean4
/-- If `t` is an antichain shadowing and including the set of maximal elements of `s`,
then `t` *is* the set of maximal elements of `s`. -/
theorem eq_setOf_maximal (ht : IsAntichain (· ≤ ·) t) (h : ∀ x, Maximal (· ∈ s) x → x ∈ t)
(hs : ∀ a ∈ t, ∃ b, b ≤ a ∧ Maximal (· ∈ s) b) : {x | Maximal (· ∈ s) x} = t :=
by
refine Set.ext fun x ↦ ⟨h _, fun hx ↦ ?_⟩
obtain ⟨y, hyx, hy⟩ := hs x hx
rwa [← ht.eq (h y hy) hx hyx]
