mlieBracketWithin_congr_mono — Mathlib

English

Equality of pullback bracket with bracket of pullbacks.

Русский

Равенство подвода скобки и скобки подвводов.

LaTeX

$$$\mathrm{mpullbackWithin}(I, I', f, \mathrm{mlieBracketWithin}(I', V, W, t), s, x_0) = \mathrm{mlieBracketWithin}(I, \mathrm{mpullbackWithin}(I, I', f, V, s), \mathrm{mpullbackWithin}(I, I', f, W, s), s, x_0)$$$

Lean4

theorem _root_.DifferentiableWithinAt.mlieBracketWithin_congr_mono
    (hV : MDifferentiableWithinAt I I.tangent (fun x ↦ (V x : TangentBundle I M)) s x) (hVs : EqOn V₁ V t)
    (hVx : V₁ x = V x) (hW : MDifferentiableWithinAt I I.tangent (fun x ↦ (W x : TangentBundle I M)) s x)
    (hWs : EqOn W₁ W t) (hWx : W₁ x = W x) (hxt : UniqueMDiffWithinAt I t x) (h₁ : t ⊆ s) :
    mlieBracketWithin I V₁ W₁ t x = mlieBracketWithin I V W s x :=
  by
  rw [mlieBracketWithin_congr hVs hVx hWs hWx]
  exact mlieBracketWithin_subset h₁ hxt hV hW

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