English
When the domain is the whole ambient space, pulling back within all of the space coincides with the standard pullback: mpullbackWithin I I' f V Set.univ = mpullback I I' f V.
Русский
Когда s равен всему пространству, вытягивание внутри совпадает с обычным вытягиванием: mpullbackWithin I I' f V Set.univ = mpullback I I' f V.
LaTeX
$$$$ \mathrm{mpullbackWithin}\ I\ I' f V \mathrm{Set.univ} = \mathrm{mpullback}\ I I' f V $$$$
Lean4
theorem mpullbackWithin_comp_of_right {g : M' → M''} {f : M → M'} {V : Π (x : M''), TangentSpace I'' x} {s : Set M}
{t : Set M'} {x₀ : M} (hg : MDifferentiableWithinAt I' I'' g t (f x₀)) (h : Set.MapsTo f s t)
(hu : UniqueMDiffWithinAt I s x₀) (hf' : (mfderivWithin I I' f s x₀).IsInvertible) :
mpullbackWithin I I'' (g ∘ f) V s x₀ = mpullbackWithin I I' f (mpullbackWithin I' I'' g V t) s x₀ :=
by
simp only [mpullbackWithin]
have hf : MDifferentiableWithinAt I I' f s x₀ := mdifferentiableWithinAt_of_isInvertible_mfderivWithin hf'
rw [mfderivWithin_comp _ hg hf h hu, IsInvertible.inverse_comp_apply_of_right hf', Function.comp_apply]
