insert_of_symmetric — Mathlib

English

If s is pairwise w.r.t. r and r is symmetric, then (insert a s) is pairwise w.r.t r provided all pairs with a from s satisfy r a b.

Русский

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

LaTeX

$$$(\text{hs}) \Rightarrow (\text{hr}) \Rightarrow (\forall b \in s, a \neq b \to r a b)$$$

Lean4

theorem insert_of_symmetric (hs : s.Pairwise r) (hr : Symmetric r) (h : ∀ b ∈ s, a ≠ b → r a b) :
    (insert a s).Pairwise r :=
  (pairwise_insert_of_symmetric hr).2 ⟨hs, h⟩

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