mpullbackWithin_eq_pullbackWithin

English

For any f, V, s, the mpullbackWithin equals the pullbackWithin: mpullbackWithin I I' f V s = pullbackWithin 𝕜 f V s.

Русский

Для любого f, V, s: mpullbackWithin I I' f V s = pullbackWithin 𝕜 f V s.

LaTeX

$$$$ \mathrm{mpullbackWithin}\ I\ I' f V s = \mathrm{pullbackWithin}\ 𝕜 f V s $$$$

Lean4

theorem mpullbackWithin_eq_pullbackWithin {f : E → E'} {V : E' → E'} {s : Set E} :
    mpullbackWithin 𝓘(𝕜, E) 𝓘(𝕜, E') f V s = pullbackWithin 𝕜 f V s :=
  by
  ext x
  simp only [mpullbackWithin, mfderivWithin_eq_fderivWithin, pullbackWithin]
  rfl

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