lieBracketWithin_congr' — Mathlib

English

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

Русский

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

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

/-- Version of `lieBracketWithin_congr` in which one assumes that the point belongs to the
given set. -/
theorem lieBracketWithin_congr' (hV : EqOn V₁ V s) (hW : EqOn W₁ W s) (hx : x ∈ s) :
    lieBracketWithin 𝕜 V₁ W₁ s x = lieBracketWithin 𝕜 V W s x :=
  lieBracketWithin_congr hV (hV hx) hW (hW hx)

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