Theorems · Theorem · logic and foundations

Set.Pairwise.insert_of_symm

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

Defined in

Mathlib.Data.Set.Pairwise.Basic

Cited by

4 results in Mathlib

Foundations

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

Assumes

Std.Symm