map_comp_map — Mathlib

English

Composition of maps in the opposite order: map g ∘ map f equals map (g ∘ f).

Русский

Составление отображений в противоположном порядке: map g ∘ map f = map (g ∘ f).

LaTeX

$$$\mathrm{WithBot.map}\ g \circ \mathrm{WithBot.map}\ f = \mathrm{WithBot.map}\ (g \circ f)$$$

Lean4

@[simp]
theorem map_comp_map (f : α → β) (g : β → γ) : WithBot.map g ∘ WithBot.map f = WithBot.map (g ∘ f) :=
  Option.map_comp_map f g

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