English
Variant: if EqOn V1 V s and EqOn W1 W s hold and x ∈ s then equality holds.
Русский
Вариант: если EqOn V1 V s и EqOn W1 W s и x ∈ s, то равенство выполняется.
LaTeX
$$Theorem mlieBracketWithin_congr' (hV: EqOn V₁ V s) (hW: EqOn W₁ W s) (hx: x ∈ s) : mlieBracketWithin I V₁ W₁ s x = mlieBracketWithin I V W s x$$
Lean4
/-- If vector fields coincide on a neighborhood of a point within a set, then the Lie brackets
also coincide on a neighborhood of this point within this set. Version where one considers the Lie
bracket within a subset. -/
theorem _root_.Filter.EventuallyEq.mlieBracketWithin_vectorField' (hV : V₁ =ᶠ[𝓝[s] x] V) (hW : W₁ =ᶠ[𝓝[s] x] W)
(ht : t ⊆ s) : mlieBracketWithin I V₁ W₁ t =ᶠ[𝓝[s] x] mlieBracketWithin I V W t :=
by
filter_upwards [hV, hW, eventually_eventually_nhdsWithin.2 hV, eventually_eventually_nhdsWithin.2 hW] with y hVy hWy
hVy' hWy'
apply Filter.EventuallyEq.mlieBracketWithin_vectorField_eq
· apply nhdsWithin_mono _ ht
exact hVy'
· exact hVy
· apply nhdsWithin_mono _ ht
exact hWy'
· exact hWy
