English
If two sets s and t are eventually equal around a point, then the Lie bracket within s equals the bracket within t at any x.
Русский
Если множества s и t совпадают из предела, то скобка Ли внутри s равна скобке внутри t в точке x.
LaTeX
$$$\text{If } s =^\mathrm{F}_{\mathcal{N}x} t,\quad \mathrm{mlieBracketWithin}(I,V,W,s,x) = \mathrm{mlieBracketWithin}(I,V,W,t,x)$$$
Lean4
/-- Variant of `mlieBracketWithin_congr_set` where one requires the sets to coincide only in
the complement of a point. -/
theorem mlieBracketWithin_congr_set' (y : M) (h : s =ᶠ[𝓝[{ y }ᶜ] x] t) :
mlieBracketWithin I V W s x = mlieBracketWithin I V W t x :=
by
simp only [mlieBracketWithin_apply]
congr 1
suffices A :
((extChartAt I x).symm ⁻¹' s ∩ range I : Set E) =ᶠ[𝓝[{(extChartAt I x) x}ᶜ] (extChartAt I x x)]
((extChartAt I x).symm ⁻¹' t ∩ range I : Set E)
by apply lieBracketWithin_congr_set' _ A
exact preimage_extChartAt_eventuallyEq_compl_singleton y h
