map_comp — Mathlib

English

If h1 and h2 are LEComap conditions for g and f respectively, then map (g ∘ f) (h1.comp h2) equals map g h1 composed with map f h2.

Русский

Если h1 и h2 заданы для g и f соответственно, то map (g ∘ f) (h1.comp h2) = map g h1 ∘ map f h2.

LaTeX

$$$$\\mathrm{map}(g \\circ f, h_1 \\cdot h_2) = \\mathrm{map}(g, h_1) \\circ \\mathrm{map}(f, h_2).$$$$

Lean4

theorem map_comp (h1 : LEComap g B C) (h2 : LEComap f A B) : map (g.comp f) (h1.comp h2) = map g h1 ∘ map f h2 :=
  by
  ext ⟨⟩
  rfl

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