Theorems · Theorem · logic and foundations

Set.pairwise_insert_of_symmetric

Deprecated since 2026-06-10Use Set.pairwise_insert_of_symm instead.

∀ {α : Type u_1} {r : α → α → Prop} {s : Set α} {a : α} [Std.Symm r],
  (insert a s).Pairwise r ↔ s.Pairwise r ∧ ∀ b ∈ s, a ≠ b → r a b

Alias of Set.pairwise_insert_of_symm.

Defined in

Mathlib.Data.Set.Pairwise.Basic

Cited by

0 results in Mathlib

Foundations

Depth 21 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Std.Symm