map_compose — Mathlib

English

Applying map twice is the same as mapping with the composed function: map m' (map m f) = map (m' ∘ m) f.

Русский

Повторное применение отображения эквивалентно отображению через композицию: map m'(map m f) = map (m' ∘ m) f.

LaTeX

$$map m' (map m f) = map (m' ∘ m) f$$

Lean4

@[simp]
theorem map_compose : Filter.map m' ∘ Filter.map m = Filter.map (m' ∘ m) :=
  funext fun _ => filter_eq <| rfl

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