uIcc_eq — Mathlib

English

The uIcc relation for multisets corresponds under the toDFinsupp equivalence to Finset.uIcc via the same embedding as in Icc_eq.

Русский

Связь uIcc для мультсет соответствует Finset uIcc через ту же вложенность, как и в Icc_eq.

LaTeX

$$$\\mathrm{uIcc}(s,t) = \\mathrm{Finset}.map(\\mathrm{equivDFinsupp.toEquiv.symm.toEmbedding})\\big(\\mathrm{Finset}.uIcc(\\mathrm{toDFinsupp}s)(\\mathrm{toDFinsupp}t)\\big)$$$

Lean4

theorem uIcc_eq : uIcc s t = (uIcc (toDFinsupp s) (toDFinsupp t)).map Multiset.equivDFinsupp.toEquiv.symm.toEmbedding :=
  (Icc_eq _ _).trans <| by simp [uIcc]

Похожие утверждения