comp — Mathlib

English

Composition of two maps corresponds to the single map of the composition of the functions: map g (map f x) = map (g ∘ f) x.

Русский

Сложение отображений соответствует композиции функций: map g (map f x) = map (g ∘ f) x.

LaTeX

$$$ \\operatorname{map} g (\\operatorname{map} f \\; x) = \\operatorname{map}(g \\circ f) \\; x $$$

Lean4

@[to_additive]
theorem comp {γ : Type w} (f : α → β) (g : β → γ) (x) : map g (map f x) = map (g ∘ f) x := by rcases x with ⟨L⟩;
  simp [Function.comp_def]

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