pairwise_insert_of_notMem — Mathlib

English

If a ∉ s, then (insert a s) is pairwise w.r.t r iff s is pairwise w.r.t r and for all b ∈ s, r a b ∧ r b a.

Русский

Если a не в s, то (insert a s) попарно по r тогда и только тогда, когда s попарно по r и для каждого b ∈ s выполняются r a b и r b a.

LaTeX

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

Lean4

theorem pairwise_insert_of_notMem (ha : a ∉ s) : (insert a s).Pairwise r ↔ s.Pairwise r ∧ ∀ b ∈ s, r a b ∧ r b a :=
  pairwise_insert.trans <| and_congr_right' <| forall₂_congr fun b hb => by simp [(ne_of_mem_of_not_mem hb ha).symm]

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