map_hcongr

Mathlib.Data.Multiset.MapFold

URI: https://scilib.ai/kg/mathlib#Multiset.map_hcongr

Lean4

theorem map_hcongr {β' : Type v} {m : Multiset α} {f : α → β} {f' : α → β'} (h : β = β') (hf : ∀ a ∈ m, f a ≍ f' a) :
    map f m ≍ map f' m := by
  subst h; simp at hf
  simp [map_congr rfl hf]

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru