map_comp_cons

Mathlib.Data.Multiset.MapFold

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

English

For any f and t, map f ∘ cons t = cons (f t) ∘ map f, i.e., applying map after adding t is the same as adding f(t) after mapping.

Русский

Для любых функций f и элемента t: map f (cons t s) = cons (f t) (map f s).

LaTeX

$$$$ \\mathrm{map}(f) \\circ \\mathrm{cons}\\ t = \\mathrm{cons}(f(t)) \\circ \\mathrm{map}(f) $$$$

Lean4

theorem map_comp_cons (f : α → β) (t) : map f ∘ cons t = cons (f t) ∘ map f :=
  by
  ext
  simp

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

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

Разделы

Аффилиация

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