map_map — Mathlib

English

Mapping a path by the identity map leaves the path unchanged.

Русский

Отображение пути константным отображением идентичности оставляет путь без изменений.

LaTeX

$$$\gamma.map(\text{continuous\_id}) = \gamma$$$

Lean4

@[simp]
theorem map_map (γ : Path x y) {Z : Type*} [TopologicalSpace Z] {f : X → Y} (hf : Continuous f) {g : Y → Z}
    (hg : Continuous g) : (γ.map hf).map hg = γ.map (hg.comp hf) :=
  by
  ext
  rfl

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