map_map — Mathlib

English

Mapping with h after mapping with g equals mapping with h ∘ g.

Русский

Отображение после отображения через g эквивалентно отображению через h ∘ g.

LaTeX

$$$\\mathrm{WithTop.map}\, h\\; (\\mathrm{WithTop.map}\\, g\\ a) = \\mathrm{WithTop.map}\\ (h \\circ g)\\ a$$$

Lean4

@[simp]
theorem map_map (h : β → γ) (g : α → β) (a : WithTop α) : map h (map g a) = map (h ∘ g) a :=
  Option.map_map h g a

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