coe_coe — Mathlib

English

Let h be a C^n-diffeomorphism between two manifolds with corners, modeled by I and I' on M and M'. Then the underlying map of h (when viewed as a function) is exactly h itself.

Русский

Пусть h — диффеоморфизм класса C^n между многообразиями с углами, моделируемыми I и I' на M и M'. Тогда отображение, лежащее в основе h и рассматриваемое как функция, совпадает с самой h.

LaTeX

$$$\text{For a } C^n\text{-diffeomorphism } h : M \to M' ,\; (h : C^n(I,M;I',M')) = h.$$$

Lean4

@[simp, norm_cast]
theorem coe_coe (h : M ≃ₘ^n⟮I, I'⟯ M') : ⇑(h : C^n⟮I, M; I', M'⟯) = h :=
  rfl

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