English
If there is a lift c from α to β with predicate p, then there is a lift from Multiset α to Multiset β given by map c, preserving the predicate ∀ x ∈ s, p x.
Русский
Если существует подъём c: α→β с предикатом p, то существует подъём Multiset α → Multiset β через map c, сохраняющий свойство ∀ x ∈ s, p x.
LaTeX
$$$$ \\mathrm{CanLift} (\\mathrm{Multiset}\\ \\alpha)(\\mathrm{Multiset}\\ \\beta)(\\mathrm{map}\\ c)\ \big(\\lambda s, \\forall x\\in s, p x\\big) $$$$
Lean4
/-- If each element of `s : Multiset α` can be lifted to `β`, then `s` can be lifted to
`Multiset β`. -/
instance canLift (c) (p) [CanLift α β c p] : CanLift (Multiset α) (Multiset β) (map c) fun s => ∀ x ∈ s, p x where
prf := by
rintro ⟨l⟩ hl
lift l to List β using hl
exact ⟨l, map_coe _ _⟩
