English
The union of two sets is a chain iff each is a chain and every cross-pair is comparable in a consistent way.
Русский
Объединение двух цепей является цепью тогда и только тогда, когда каждая из них цепь и любая пара по-разному находится в отношении.
LaTeX
$$$\operatorname{IsChain}(r, s \cup t) \iff \operatorname{IsChain}(r,s) \land \operatorname{IsChain}(r,t) \land \forall a\in s\,\forall b\in t\,(a\neq b \rightarrow r a b \lor r b a)$$$
Lean4
theorem isChain_union {s t : Set α} :
IsChain r (s ∪ t) ↔ IsChain r s ∧ IsChain r t ∧ ∀ a ∈ s, ∀ b ∈ t, a ≠ b → r a b ∨ r b a := by
rw [IsChain, IsChain, IsChain, pairwise_union_of_symmetric fun _ _ ↦ Or.symm]
