map_map — Mathlib

English

For outer measures m on α and functions f : α → β and g : β → γ, map g (map f m) = map (g ∘ f) m.

Русский

Для внешних мер m на α и функций f : α → β, g : β → γ выполняется map g (map f m) = map (g ∘ f) m.

LaTeX

$$$ map\ g\ (map\ f\ m) = map\ (g \circ f)\ m $$$

Lean4

@[simp]
theorem map_map {β γ} (f : α → β) (g : β → γ) (m : OuterMeasure α) : map g (map f m) = map (g ∘ f) m :=
  ext fun _ => rfl

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