Theorems · Theorem · order theory

Multiset.uIcc_eq

∀ {α : Type u_1} [inst : DecidableEq α] (s t : Multiset α),
  Finset.uIcc s t =
    Finset.map Multiset.equivDFinsupp.symm.toEmbedding (Finset.uIcc (Multiset.toDFinsupp s) (Multiset.toDFinsupp t))

Defined in: Mathlib.Data.Multiset.Interval
Cited by: 1 results in Mathlib
Foundations: Depth 88 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: DecidableEq

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites17

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coestatement and proof · cited by 62,936
Finsetstatement · cited by 13,712
Equiv.symmstatement and proof · cited by 3,681
AddMonoidHomstatement · cited by 3,230
Multisetstatement and proof · cited by 2,627
Finset.mapstatement and proof · cited by 747
DFinsuppstatement · cited by 694
Finset.Iccproof · cited by 348
Equiv.toEmbeddingstatement and proof · cited by 254
AddEquiv.toEquivstatement · cited by 174
EquivLike.toEquivproof · cited by 125
Finset.uIccstatement · cited by 84

Cited by1

Results whose statement or proof uses this declaration.

Multiset.card_uIccproof · cited by 0