mlieBracketWithin_eq_zero_of_eq_zero

English

On the whole space, the Lie bracket within equals the Lie bracket.

Русский

На всей области скобка Ли внутри совпадает со скобкой Ли вообще.

LaTeX

$$mlieBracketWithin_univ : mlieBracketWithin I V W univ = mlieBracket I V W$$

Lean4

theorem mlieBracketWithin_eq_zero_of_eq_zero (hV : V x = 0) (hW : W x = 0) : mlieBracketWithin I V W s x = 0 :=
  by
  simp only [mlieBracketWithin, mpullback_apply]
  rw [lieBracketWithin_eq_zero_of_eq_zero]
  · simp
  · simp only [mpullbackWithin_apply]
    have : (extChartAt I x).symm ((extChartAt I x) x) = x := by simp
    rw [this, hV]
    simp
  · simp only [mpullbackWithin_apply]
    have : (extChartAt I x).symm ((extChartAt I x) x) = x := by simp
    rw [this, hW]
    simp

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