lieBracketWithin_inter — Mathlib

English

If t ∈ 𝓝 x, then lieBracketWithin 𝕜 V W (s ∩ t) x = lieBracketWithin 𝕜 V W s x.

Русский

Если t принадлежит 𝓝 x, то скобка внутри s ∩ t равна скобке внутри s в x.

LaTeX

$$$(ht: t \\in 𝓝 x) \\Rightarrow lieBracketWithin 𝕜 V W (s \\cap t) x = lieBracketWithin 𝕜 V W s x$$$

Lean4

theorem lieBracketWithin_inter (ht : t ∈ 𝓝 x) : lieBracketWithin 𝕜 V W (s ∩ t) x = lieBracketWithin 𝕜 V W s x := by
  simp [lieBracketWithin, fderivWithin_inter, ht]

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