mlieBracketWithin_congr_set — Mathlib

English

A variant of the set-congruence principle: if s and t agree outside a single point, the Lie bracket within s and within t agree at any x.

Русский

Вариант принципа совпадения множеств: если s и t совпадают вне одной точки, то скобка Ли внутри s и внутри t одинакова в x.

LaTeX

$$$\text{If } s =^\mathrm{F}_{\mathcal{N}({y})^c} t,\quad \mathrm{mlieBracketWithin}(I,V,W,s,x) = \mathrm{mlieBracketWithin}(I,V,W,t,x)$$$

Lean4

theorem mlieBracketWithin_congr_set (h : s =ᶠ[𝓝 x] t) : mlieBracketWithin I V W s x = mlieBracketWithin I V W t x :=
  mlieBracketWithin_congr_set' x <| h.filter_mono inf_le_left

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