map_map — Mathlib

English

Pushforward along m and then along n equals pushforward along n ∘ m: f.map m).map n = f.map (n ∘ m).

Русский

Перенос по функции m, затем по n равен переносу по композиции n ∘ m: f.map m).map n = f.map (n ∘ m).

LaTeX

$$$\forall f:\mathrm{Ultrafilter}(\alpha),\forall m:\alpha\to\beta,\forall n:\beta\to\gamma,\ (f.map\ m).map\ n = f.map\ (n \circ m)$$$

Lean4

@[simp]
nonrec theorem map_map (f : Ultrafilter α) (m : α → β) (n : β → γ) : (f.map m).map n = f.map (n ∘ m) :=
  coe_injective map_map

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