English
IsStrongAntichain r (insert a s) holds iff IsStrongAntichain r s holds and for all b ∈ s with a ≠ b and all c, not r a c or not r b c.
Русский
IsStrongAntichain r (insert a s) эквивалентно IsStrongAntichain r s и для всех b ∈ s, a ≠ b, и для всех c выполняется либо не r a c, либо не r b c.
LaTeX
$$$\\text{IsStrongAntichain}(r, \\operatorname{Set.insert.insert}(a,s)) \\iff \\text{IsStrongAntichain}(r, s) \\land \\forall b (b \\in s \\rightarrow a \\neq b \\rightarrow \\forall c, \\lnot r a c \\lor \\lnot r b c)$$$
Lean4
theorem _root_.isStrongAntichain_insert :
IsStrongAntichain r (insert a s) ↔ IsStrongAntichain r s ∧ ∀ ⦃b⦄, b ∈ s → a ≠ b → ∀ c, ¬r a c ∨ ¬r b c :=
Set.pairwise_insert_of_symmetric fun _ _ h c => (h c).symm
