English
For sets s,t, the union s ∪ t is an antichain with respect to r if and only if s and t are antichains and all cross-pairs are incomparable in the appropriate sense.
Русский
Для множеств s,t объединение s ∪ t является антицепочкой по отношению r тогда и только тогда, когда сами s,t — антицепочки и все попарные кросс-пары несравнимы в нужном смысле.
LaTeX
$$$IsAntichain(r)(s\cup t) \iff (IsAntichain(r)s) \land (IsAntichain(r)t) \land \forall a\in s\,\forall b\in t\; a\neq b \rightarrow r^{c}a b \land r^{c}b a$$$
Lean4
theorem isAntichain_union :
IsAntichain r (s ∪ t) ↔ IsAntichain r s ∧ IsAntichain r t ∧ ∀ a ∈ s, ∀ b ∈ t, a ≠ b → rᶜ a b ∧ rᶜ b a := by
rw [IsAntichain, IsAntichain, IsAntichain, pairwise_union]
