Theorems · Theorem · combinatorics

Multiset.mem_sort

∀ {α : Type u_1} {a : α} {s : Multiset α} (r : α → α → Prop) [inst : DecidableRel r] [inst_1 : IsTrans α r]
  [inst_2 : Std.Antisymm r] [inst_3 : Std.Total r], a ∈ s.sort r ↔ a ∈ s

Defined in

Mathlib.Data.Multiset.Sort

Cited by

1 results in Mathlib

Foundations

Depth 61 from the axioms · uses propext, Quot.sound

Assumes

DecidableRelIsTransStd.AntisymmStd.Total