insert_of_symmetric_of_notMem — Mathlib

English

If s is pairwise w.r.t r and every b ∈ s has r a b and r b a, then insert a into s is pairwise w.r.t r.

Русский

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

LaTeX

$$$\forall {s : Set \alpha} (a : \alpha), s.Pairwise r \to (\forall b \in s, a \neq b \to r a b \land r b a) \to (insert a s).Pairwise r$$$

Lean4

@[deprecated Pairwise.insert_of_symmetric (since := "2025-03-19")]
theorem insert_of_symmetric_of_notMem (hs : s.Pairwise r) (hr : Symmetric r) (ha : a ∉ s) (h : ∀ b ∈ s, r a b) :
    (insert a s).Pairwise r :=
  (pairwise_insert_of_symmetric_of_notMem hr ha).2 ⟨hs, h⟩

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