comp_map — Mathlib

English

Mapping with a composition is the same as mapping in two steps with the composed function.

Русский

Отображение через композицию эквивалентно последовательному отображению через составляющие функции.

LaTeX

$$$ t.map(g \circ f) = (t.map f).map g $$$

Lean4

theorem comp_map {β γ : Type*} (f : α → β) (g : β → γ) (t : Tree α) : t.map (g ∘ f) = (t.map f).map g := by
  induction t with
  | nil => rw [map, map, map]
  | node v l r hl hr => rw [map, map, map, hl, hr, Function.comp_apply]

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