lieBracketWithin_congr — Mathlib

English

If V₁ ≡ V s and W₁ ≡ W s, then lieBracketWithin 𝕜 V₁ W₁ s x = lieBracketWithin 𝕜 V W s x.

Русский

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

LaTeX

$$$(hV: Set.EqOn V₁ V s) \\land (hVx: V₁ x = V x) \\land (hW: Set.EqOn W₁ W s) \\land (hWx: W₁ x = W x) \\Rightarrow lieBracketWithin 𝕜 V₁ W₁ s x = lieBracketWithin 𝕜 V W s x$$$

Lean4

theorem lieBracketWithin_congr (hV : EqOn V₁ V s) (hVx : V₁ x = V x) (hW : EqOn W₁ W s) (hWx : W₁ x = W x) :
    lieBracketWithin 𝕜 V₁ W₁ s x = lieBracketWithin 𝕜 V W s x :=
  (hV.eventuallyEq.filter_mono inf_le_right).lieBracketWithin_vectorField_eq hVx
    (hW.eventuallyEq.filter_mono inf_le_right) hWx

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