range_eq_target — Mathlib

English

The model-with-corners can be viewed as a function from the manifold to its ambient space; this coercion is canonical and compatible with the partial equivalence structure.

Русский

Модель с углами можно рассматривать как отображение из многообразия в окружающее пространство; это канонический переход, совместимый с частичной эквалентной структурой.

LaTeX

$$$\\text{toFun'}: ModelWithCorners 𝕜 E H \\to H \\to E$$$

Lean4

theorem range_eq_target {𝕜 E H : Type*} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E]
    [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) : range I.toPartialEquiv = I.target := by
  rw [← I.image_source_eq_target, I.source_eq, image_univ.symm]

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