English
The inverse mapping of a model-with-corners is registered as a partial equivalence; its symmetry provides a well-defined inverse map between the spaces.
Русский
Обратное отображение модели с углами регистрируется как частичное эквалентное отображение; его симметрия задаёт корректную обратную связь между пространствами.
LaTeX
$$$\\text{symm}: PartialEquiv E H$$$
Lean4
/-- If a model with corners has full range, the `convex_range'` condition is satisfied. -/
def of_target_univ (𝕜 : Type*) [NontriviallyNormedField 𝕜] {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
{H : Type*} [TopologicalSpace H] (φ : PartialEquiv H E) (hsource : φ.source = univ) (htarget : φ.target = univ)
(hcont : Continuous φ) (hcont_inv : Continuous φ.symm) : ModelWithCorners 𝕜 E H
where
toPartialEquiv := φ
source_eq := hsource
convex_range' :=
by
have : range φ = φ.target := by rw [← φ.image_source_eq_target, hsource, image_univ.symm]
simp only [this, htarget, dite_else_true]
intro h
letI := h.rclike 𝕜
letI := NormedSpace.restrictScalars ℝ 𝕜 E
exact convex_univ
nonempty_interior' :=
by
have : range φ = φ.target := by rw [← φ.image_source_eq_target, hsource, image_univ.symm]
simp [this, htarget]
