map_lift — Mathlib

English

For any path P0 and a map f, the class of the mapped path equals the image of the class under mapFn: ⟦P0.map f⟧ = Quotient.mapFn ⟦P0⟧ f.

Русский

Для любого пути P0 и отображения f, класс образа пути равен образу класса под mapFn.

LaTeX

$$$\langle P_0.map f\rangle = \operatorname{Quotient.mapFn} \langle P_0\rangle f$$$

Lean4

theorem map_lift (P₀ : Path x₀ x₁) (f : C(X, Y)) : ⟦P₀.map f.continuous⟧ = Quotient.mapFn ⟦P₀⟧ f :=
  rfl

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