English
Let l be a finite list of elements of a type α and s be a multisubset of α. Then s is a member of the collection of submultisets of l if and only if s is a submultiset of the multiset represented by l; equivalently, s ≤ ofList(l).
Русский
Пусть l — конечный список элементов α, а s — мультимножество α. Тогда s является элементом множества подмультимножеств l тогда и только тогда, когда s является подмультимножеством мультимножества, соответствующего l; то есть s ≤ ofList(l).
LaTeX
$$$ s \\in \\mathrm{powersetAux}(l) \\iff s \\le \\operatorname{ofList}(l) $$$
Lean4
@[simp]
theorem mem_powersetAux {l : List α} {s} : s ∈ powersetAux l ↔ s ≤ ↑l :=
Quotient.inductionOn s <| by simp [powersetAux_eq_map_coe, Subperm, and_comm]
