insert — Mathlib

English

If r is symmetric, insert preserves pairwise property with a relaxed condition: (insert a s) is pairwise w.r.t r iff s is pairwise w.r.t r and a ≠ b implies r a b for all b ∈ s.

Русский

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

LaTeX

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

Lean4

protected theorem insert (hs : s.Pairwise r) (h : ∀ b ∈ s, a ≠ b → r a b ∧ r b a) : (insert a s).Pairwise r :=
  pairwise_insert.2 ⟨hs, h⟩

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