Theorems · Theorem · combinatorics

Multiset.map_eq_map_of_bij_of_nodup

∀ {α : Type u_1} {β : Type v} {γ : Type u_2} (f : α → γ) (g : β → γ) {s : Multiset α} {t : Multiset β},
  s.Nodup →
    t.Nodup →
      ∀ (i : (a : α) → a ∈ s → β),
        (∀ (a : α) (ha : a ∈ s), i a ha ∈ t) →
          (∀ (a₁ : α) (ha₁ : a₁ ∈ s) (a₂ : α) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂) →
            (∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), i a ha = b) →
              (∀ (a : α) (ha : a ∈ s), f a = g (i a ha)) → Multiset.map f s = Multiset.map g t

Defined in

Mathlib.Data.Multiset.MapFold

Cited by

3 results in Mathlib

Foundations

Depth 52 from the axioms · uses propext, Classical.choice, Quot.sound