mlieBracketWithin_vectorField_eq_of_mem

English

Variant: if sets s,t agree outside y, the bracket within s and within t agree at x.

Русский

Вариант: если s,t совпадают вне y, скобка внутри s и внутри t совпадают в x.

LaTeX

$$$\text{EqOn } V₁ V s \to\; \text{EqOn } W₁ W s \to\; y \in M \Rightarrow \mathrm{mlieBracketWithin}(I,V₁,W₁,s,x) = \mathrm{mlieBracketWithin}(I,V,W,s,x)$$$

Lean4

theorem _root_.Filter.EventuallyEq.mlieBracketWithin_vectorField_eq_of_mem (hV : V₁ =ᶠ[𝓝[s] x] V) (hW : W₁ =ᶠ[𝓝[s] x] W)
    (hx : x ∈ s) : mlieBracketWithin I V₁ W₁ s x = mlieBracketWithin I V W s x :=
  hV.mlieBracketWithin_vectorField_eq (mem_of_mem_nhdsWithin hx hV :) hW (mem_of_mem_nhdsWithin hx hW :)

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