pmap — Mathlib

Lean4
/-- Lift of the list `pmap` operation. Map a partial function `f` over a multiset
  `s` whose elements are all in the domain of `f`. -/
nonrec def pmap {p : α → Prop} (f : ∀ a, p a → β) (s : Multiset α) : (∀ a ∈ s, p a) → Multiset β :=
  Quot.recOn s (fun l H => ↑(pmap f l H)) fun l₁ l₂ (pp : l₁ ~ l₂) =>
    funext fun H₂ : ∀ a ∈ l₂, p a =>
      have H₁ : ∀ a ∈ l₁, p a := fun a h => H₂ a (pp.subset h)
      have :
        ∀ {s₂ e H},
          @Eq.ndrec (Multiset α) l₁ (fun s => (∀ a ∈ s, p a) → Multiset β) (fun _ => ↑(pmap f l₁ H₁)) s₂ e H =
            ↑(pmap f l₁ H₁) :=
        by intro s₂ e _; subst e; rfl
      this.trans <| Quot.sound <| pp.pmap f
Похожие утверждения