English
If r is symmetric, then (s ∪ t) is pairwise w.r.t r iff s and t are pairwise and any cross pair satisfies r a b.
Русский
Если r симметрично, тогда (s ∪ t) попарно по r тогда и только тогда, когда s и t попарны и любые перекрестные пары удовлетворяют r a b.
LaTeX
$$$(\,s \cup t\,).Pairwise r \leftrightarrow s.Pairwise r \land t.Pairwise r \land \forall a \in s, \forall b \in t, a \neq b \to r a b$$$
Lean4
theorem pairwise_union_of_symmetric (hr : Symmetric r) :
(s ∪ t).Pairwise r ↔ s.Pairwise r ∧ t.Pairwise r ∧ ∀ a ∈ s, ∀ b ∈ t, a ≠ b → r a b :=
pairwise_union.trans <| by simp only [hr.iff, and_self_iff]