theorem OpenPartialHomeomorph.exists_contDiff_source_univ_target_subset_ball {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] (c : F) (r : ℝ) : ∃ (f : OpenPartialHomeomorph F F), ContDiff ℝ ↑⊤ ↑f ∧ ContDiffOn ℝ (↑⊤) (↑f.symm) f.target ∧ f.source = Set.univ ∧ (0 < r → f.target ⊆ Metric.ball c r) ∧ ↑f 0 = c

noncomputable def diffeomorphToNhd {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] (c : F) (r : ℝ) : OpenPartialHomeomorph F F

A variant of InnerProductSpace.diffeomorphToNhd which provides a function satisfying the weaker condition range_diffeomorph_to_nhd_subset_ball but which applies to any NormedSpace.

In fact one could demand this stronger property but it would be more work and we don't need it.

Equations

• diffeomorphToNhd c r = ⋯.choose

@[simp]

theorem diffeomorphToNhd_source {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] (c : F) (r : ℝ) : (diffeomorphToNhd c r).source = Set.univ

@[simp]

theorem diffeomorphToNhd_apply_zero {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] (c : F) (r : ℝ) : ↑(diffeomorphToNhd c r) 0 = c

theorem target_diffeomorphToNhd_subset_ball {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] (c : F) {r : ℝ} (hr : 0 < r) : (diffeomorphToNhd c r).target ⊆ Metric.ball c r

@[simp]

theorem range_diffeomorphToNhd_subset_ball {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] (c : F) {r : ℝ} (hr : 0 < r) : Set.range ↑(diffeomorphToNhd c r) ⊆ Metric.ball c r

@[simp]

theorem contDiff_diffeomorphToNhd {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] (c : F) (r : ℝ) {n : ℕ∞} : ContDiff ℝ ↑n ↑(diffeomorphToNhd c r)

@[simp]

theorem contDiffOn_diffeomorphToNhd_inv {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] (c : F) (r : ℝ) {n : ℕ∞} : ContDiffOn ℝ (↑n) (↑(diffeomorphToNhd c r).symm) (diffeomorphToNhd c r).target