map_univ_comp_coe — Mathlib

English

Composing a finite-set map with the embedding yields the same as direct mapping to α.

Русский

Составление отображения Finset → α через вложение эквивалентно прямому отображению в α.

LaTeX

$$((Finset.univ : Finset m).val.map (f ∘ (fun x : m ↦ (x : α)))) = m.map f$$

Lean4

theorem map_univ_comp_coe {β : Type*} (m : Multiset α) (f : α → β) :
    ((Finset.univ : Finset m).val.map (f ∘ (fun x : m ↦ (x : α)))) = m.map f := by
  rw [← Multiset.map_map, Multiset.map_univ_coe]

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