English
Let s be a weak antichain with respect to a given preorder, and let a be a new element such that for every b in s with b ≠ a, neither b ≺ a nor a ≺ b holds. Then the set obtained by inserting a into s is again a weak antichain.
Русский
Пусть S — слабая антицепь относительно заданного предварительного порядка, и пусть a — новый элемент such that для каждого b ∈ S с b ≠ a верно, что ни b ≺ a, ни a ≺ b. Тогда множество, полученное добавлением a к S, снова является слабой антицепью.
LaTeX
$$$\mathrm{IsWeakAntichain}(s) \to (\forall b\in s, a \neq b \to \neg (b \\prec a)) \to (\forall b\in s, a \neq b \to \neg (a \\prec b)) \to \mathrm{IsWeakAntichain}(s\cup\{a\})$$$
Lean4
protected theorem insert (hs : IsWeakAntichain s) :
(∀ ⦃b⦄, b ∈ s → a ≠ b → ¬b ≺ a) → (∀ ⦃b⦄, b ∈ s → a ≠ b → ¬a ≺ b) → IsWeakAntichain (insert a s) :=
IsAntichain.insert hs
