mlieBracketWithin_def — Mathlib

English

The constructed Lie bracket within equals the standard Lie bracket on the manifold when restricted to the ambient model spaces.

Русский

Сконструированная внутри скобка Ли равна стандартной скобке Ли на касательном многообразии при ограничении до окружающих модельных пространств.

LaTeX

$$mlieBracketWithin I V W s = lieBracketWithin 𝕜 V W s$$

Lean4

theorem mlieBracketWithin_def :
    mlieBracketWithin I V W s = fun x₀ ↦
      mpullback I 𝓘(𝕜, E) (extChartAt I x₀)
        (lieBracketWithin 𝕜 (mpullbackWithin 𝓘(𝕜, E) I (extChartAt I x₀).symm V (range I))
          (mpullbackWithin 𝓘(𝕜, E) I (extChartAt I x₀).symm W (range I)) ((extChartAt I x₀).symm ⁻¹' s ∩ range I))
        x₀ :=
  rfl

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