canLiftFinset — Mathlib

English

There is a canonical way to go from a nodup Multiset α to a Finset α: if m is a Multiset with Nodup, then there exists a Finset s with s.val = m.

Русский

Существует канонический переход от бездубликатного мультимножества α к Finset α: если m ∈ Multiset α и m.Nodup, тогда существует Finset s с s.val = m.

LaTeX

$$$ \forall m : \mathrm{Multiset} \alpha, m.\mathrm{Nodup} \Rightarrow \exists s : \mathrm{Finset} \alpha, s.\mathrm{val} = m $$$

Lean4

instance canLiftFinset {α} : CanLift (Multiset α) (Finset α) Finset.val Multiset.Nodup :=
  ⟨fun m hm => ⟨⟨m, hm⟩, rfl⟩⟩

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