map_join — Mathlib

English

Let f: α → β and S be a multisets-of-multisets of α. Then map f distributes over the join: map f (join S) = join (map (map f) S).

Русский

Пусть f: α → β и S — мультимножество над мультимножествами α. Тогда отображение f распространяется через объединение: map f (join S) = join (map (map f) S).

LaTeX

$$$map f (join S) = join (map (map f) S)$$$

Lean4

@[simp]
theorem map_join (f : α → β) (S : Multiset (Multiset α)) : map f (join S) = join (map (map f) S) := by
  induction S using Multiset.induction with
  | empty => simp
  | cons _ _ ih => simp [ih]

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