toPrefunctor_comp — Mathlib

English

Let f: α → β and g: β → γ be functions between types. Then the prefunctor corresponding to g ∘ f is equal to the composition of the prefunctors corresponding to f and g.

Русский

Пусть f: α → β и g: β → γ — отображения между типами. Тогда предфунктор, соответствующий композиции g ∘ f, равен композиции предфункторов, соответствующих f и g.

LaTeX

$$$ \\operatorname{toPrefunctor}(g \\circ f) = \\operatorname{toPrefunctor}(f) \\, ⋙q \\, \\operatorname{toPrefunctor}(g) $$$

Lean4

theorem toPrefunctor_comp (f : α → β) (g : β → γ) : toPrefunctor (g ∘ f) = toPrefunctor f ⋙q toPrefunctor g :=
  rfl

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