English
If EqOn V1 V s and EqOn W1 W s hold and the point x lies in s, then the Lie brackets agree: mlieBracketWithin I V1 W1 s x = mlieBracketWithin I V W s x.
Русский
Если V1,V и W1,W совпадают на s и x∈s, то скобки совпадают.
LaTeX
$$$\text{EqOn } V₁ V s \to\; \text{EqOn } W₁ W s \to\; x \in s \Rightarrow \mathrm{mlieBracketWithin}(I,V₁,W₁,s,x) = \mathrm{mlieBracketWithin}(I,V,W,s,x)$$$
Lean4
theorem _root_.Filter.EventuallyEq.mlieBracketWithin_vectorField_eq (hV : V₁ =ᶠ[𝓝[s] x] V) (hxV : V₁ x = V x)
(hW : W₁ =ᶠ[𝓝[s] x] W) (hxW : W₁ x = W x) : mlieBracketWithin I V₁ W₁ s x = mlieBracketWithin I V W s x :=
by
simp only [mlieBracketWithin_apply]
congr 1
let I1 : NormedAddCommGroup (TangentSpace 𝓘(𝕜, E) (extChartAt I x x)) := inferInstanceAs (NormedAddCommGroup E)
let _I2 : NormedSpace 𝕜 (TangentSpace 𝓘(𝕜, E) (extChartAt I x x)) := inferInstanceAs (NormedSpace 𝕜 E)
apply Filter.EventuallyEq.lieBracketWithin_vectorField_eq
· apply nhdsWithin_mono _ inter_subset_left
filter_upwards [(continuousAt_extChartAt_symm x).continuousWithinAt.preimage_mem_nhdsWithin'' hV (by simp)] with y
hy
simp only [mpullbackWithin_apply]
congr 1
· simp only [mpullbackWithin_apply]
congr 1
convert hxV <;> exact extChartAt_to_inv x
· apply nhdsWithin_mono _ inter_subset_left
filter_upwards [(continuousAt_extChartAt_symm x).continuousWithinAt.preimage_mem_nhdsWithin'' hW (by simp)] with y
hy
simp only [mpullbackWithin_apply]
congr 1
· simp only [mpullbackWithin_apply]
congr 1
convert hxW <;> exact extChartAt_to_inv x
