setOf_riemannianEDist_lt_subset_nhds'

English

For a path γ:ℝ→M with ENorm data along γ, the path-length equals the lintegral over [a,b] of the ENorm of the mfderiv along γ.

Русский

Длина пути равна лин-интегралу по интервалу [a,b] от нормы mfderiv вдоль γ.

LaTeX

$$$$\\operatorname{pathELength}(I,\\gamma,a,b)=\\int_{a}^{b} \\|\\mathrm{mfderiv}(I,\\gamma(t))\\| \\, dt.$$$$

Lean4

/-- Any neighborhood of `x` contains all the points which are close enough to `x` for the
Riemannian distance, `ℝ≥0∞` version. -/
theorem setOf_riemannianEDist_lt_subset_nhds' [RegularSpace M] {x : M} {s : Set M} (hs : s ∈ 𝓝 x) :
    ∃ c > 0, {y | riemannianEDist I x y < c} ⊆ s :=
  by
  rcases setOf_riemannianEDist_lt_subset_nhds I hs with ⟨c, c_pos, hc⟩
  exact ⟨c, mod_cast c_pos, hc⟩

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