mlieBracket_vectorField_eq — Mathlib

English

If EqOn for V₁,V and W₁,W on s and x ∈ s then equality holds for the Lie bracket within s at x.

Русский

Если EqOn для V₁,V и W₁,W на s и x ∈ s, то равенство скобки внутри s в x выполняется.

LaTeX

$$EqOn V₁ V s → EqOn W₁ W s → Set.InstMembership.mem s x → Eq (mlieBracketWithin I V₁ W₁ s x) (mlieBracketWithin I V W s x)$$

Lean4

theorem _root_.Filter.EventuallyEq.mlieBracket_vectorField_eq (hV : V₁ =ᶠ[𝓝 x] V) (hW : W₁ =ᶠ[𝓝 x] W) :
    mlieBracket I V₁ W₁ x = mlieBracket I V W x := by
  rw [← mlieBracketWithin_univ, ← mlieBracketWithin_univ, hV.mlieBracketWithin_vectorField_eq_nhds hW]

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