mlieBracketWithin_vectorField — Mathlib

English

If vector fields V₁ and W₁ coincide on the neighborhood of x relative to insert x s, then the bracket equals the original bracket on s.

Русский

Если V₁ и W₁ совпадают в окрестности x после вставки x в s, то скобка равна исходной скобке на s.

LaTeX

$$$\mathrm{mlieBracketWithin}(I,V₁,W₁,s,x) = \mathrm{mlieBracketWithin}(I,V,W,s,x)$ under insertion of x into s$$

Lean4

protected theorem _root_.Filter.EventuallyEq.mlieBracketWithin_vectorField (hV : V₁ =ᶠ[𝓝[s] x] V)
    (hW : W₁ =ᶠ[𝓝[s] x] W) : mlieBracketWithin I V₁ W₁ s =ᶠ[𝓝[s] x] mlieBracketWithin I V W s :=
  hV.mlieBracketWithin_vectorField' hW Subset.rfl

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