map_comp_map — Mathlib

English

If two composed maps agree, then applying them to the same input yields equal results after mapping twice.

Русский

Если две составные отображения совпадают, то применение их к одному и тому же элементу даёт одинаковый результат после отображения дважды.

LaTeX

$$$\\forall a:\\; \\mathrm{WithTop.map}\\, g_1(\\mathrm{WithTop.map}\\, f_1(a)) = \\mathrm{WithTop.map}\\, g_2(\\mathrm{WithTop.map}\\, f_2(a))$ при условии $g_1 \\circ f_1 = g_2 \\circ f_2$$$

Lean4

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

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