pairwise_insert — Mathlib

English

The insert of a into s is pairwise w.r.t r iff s is pairwise w.r.t r and every element b of s with a ≠ b satisfies r a b and r b a.

Русский

Добавление элемента a в множество s попарно по r тогда и только тогда, когда s попарно по r и для каждого b∈s, b ≠ a, выполняются r a b и r b a.

LaTeX

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

Lean4

theorem pairwise_insert : (insert a s).Pairwise r ↔ s.Pairwise r ∧ ∀ b ∈ s, a ≠ b → r a b ∧ r b a := by
  simp only [insert_eq, pairwise_union, pairwise_singleton, true_and, mem_singleton_iff, forall_eq]

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