insert_of_notMem — Mathlib

English

If r is symmetric and a ∉ s, then (insert a s) is pairwise w.r.t r iff s is pairwise w.r.t r and every b ∈ s satisfies r a b.

Русский

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

LaTeX

$$$(\text{hr}) \Rightarrow ((insert a s).Pairwise r) \leftrightarrow (s.Pairwise r \land \forall b \in s, r a b)$$$

Lean4

theorem insert_of_notMem (ha : a ∉ s) (hs : s.Pairwise r) (h : ∀ b ∈ s, r a b ∧ r b a) : (insert a s).Pairwise r :=
  (pairwise_insert_of_notMem ha).2 ⟨hs, h⟩

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