eventually_enorm_mfderivWithin_symm_extChartAt_lt

English

For any x and any c>0 (as an extended nonnegative real), the riemannian distance between x and nearby points is eventually less than c.

Русский

Для любой точки x и любого c>0 (в контексте riemannian distance), расстояние к соседним точкам становится меньше c; это локальная аппроксимация.

LaTeX

$$$$\\forall c>0,\\; \\text{eventually }(y\\mapsto \\operatorname{riemannianEDist}(I,x,y) < c)\\text{ near }x.$$$$

Lean4

theorem eventually_enorm_mfderivWithin_symm_extChartAt_lt (x : M) :
    ∃ C > (0 : ℝ≥0),
      ∀ᶠ y in 𝓝[range I] (extChartAt I x x), ‖mfderivWithin 𝓘(ℝ, E) I (extChartAt I x).symm (range I) y‖ₑ < C :=
  by
  rcases eventually_norm_mfderivWithin_symm_extChartAt_lt I x with ⟨C, C_pos, hC⟩
  lift C to ℝ≥0 using C_pos.le
  simp only [gt_iff_lt, NNReal.coe_pos] at C_pos
  refine ⟨C, C_pos, ?_⟩
  filter_upwards [hC] with y hy
  simp only [enorm, nnnorm]
  exact_mod_cast hy

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