Theorems · Theorem · logic and foundations

Set.pairwise_insert_of_symm

∀ {α : 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

Defined in

Mathlib.Data.Set.Pairwise.Basic

Cited by

10 results in Mathlib

Foundations

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

Assumes

Std.Symm