modelWithCornersSelf — Mathlib

English

For a model-with-corners I, the image/range of the nondegenerate map equals the target space; this shows the map is surjective onto the model target.

Русский

Для модели с углами образ/диапазон ненулевой карты совпадает с целевым пространством; карта сюръективна на цель модели.

LaTeX

$$$\\operatorname{range} I.toPartialEquiv = I.target$$$

Lean4

/-- A vector space is a model with corners, denoted as `𝓘(𝕜, E)` within the `Manifold` namespace. -/
def modelWithCornersSelf (𝕜 : Type*) [NontriviallyNormedField 𝕜] (E : Type*) [NormedAddCommGroup E] [NormedSpace 𝕜 E] :
    ModelWithCorners 𝕜 E E :=
  ModelWithCorners.of_target_univ 𝕜 (PartialEquiv.refl E) rfl rfl continuous_id continuous_id

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