pairwise_union — Mathlib

English

The union s ∪ t is pairwise with respect to r iff s and t are pairwise and every cross pair with a ∈ s, b ∈ t with a ≠ b satisfies r a b and r b a.

Русский

Объединение s ∪ t попарно по r тогда, когда оба множества попарно по r и каждое попарное несовместимое перекрестное пара a∈s, b∈t удовлетворяет r a b и r b a.

LaTeX

$$$(s \cup t).Pairwise r \iff s.Pairwise r \land t.Pairwise r \land \forall a \in s, \forall b \in t, a \neq b \to r a b \land r b a$$$

Lean4

theorem pairwise_union : (s ∪ t).Pairwise r ↔ s.Pairwise r ∧ t.Pairwise r ∧ ∀ a ∈ s, ∀ b ∈ t, a ≠ b → r a b ∧ r b a :=
  by
  simp only [Set.Pairwise, mem_union, or_imp, forall_and]
  aesop

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