lieBracketWithin_congr_set — Mathlib

English

If V₁, W₁ coincide with V, W on s, and x ∈ s, then lieBracketWithin 𝕜 V₁ W₁ s x = lieBracketWithin 𝕜 V W s x.

Русский

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

LaTeX

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

Lean4

theorem lieBracketWithin_congr_set (h : s =ᶠ[𝓝 x] t) : lieBracketWithin 𝕜 V W s x = lieBracketWithin 𝕜 V W t x :=
  lieBracketWithin_congr_set' x <| h.filter_mono inf_le_left

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