pairwise_union_of_symmetric — Mathlib

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]

Похожие утверждения