map_const — Mathlib

English

Applying a constant function to all elements yields a replicate of that constant with length equal to the cardinality of s.

Русский

Применение константной функции ко всем элементам даёт повторение константы столько раз, сколько элементов в s.

LaTeX

$$$$ \\operatorname{map}(\\lambda x. b) s = \\operatorname{replicate}(\\operatorname{card} s) b $$$$

Lean4

theorem map_const (s : Multiset α) (b : β) : map (const α b) s = replicate (card s) b :=
  Quot.inductionOn s fun _ => congr_arg _ List.map_const'

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