coe_mk — Mathlib

English

A path γ from x to y, viewed as a continuous map from I to X, is equal to the path γ itself when coerced to a continuous map.

Русский

Путь γ от x к y, рассматриваемый как непрерывная карта I → X, равен самому γ при преобразовании к непрерывной карте.

LaTeX

$$$ (\\gamma : C(I,X)) = γ $$$

Lean4

/-- A special version of `ContinuousMap.coe_coe`.

When you delete this deprecated lemma, please rename `Path.coe_mk'` to `Path.coe_mk`. -/
@[deprecated ContinuousMap.coe_coe (since := "2025-05-02")]
theorem coe_mk : ⇑(γ : C(I, X)) = γ :=
  rfl

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