mpullbackWithin_id — Mathlib

English

The mpullbackWithin for Euclidean model with corners equals pullbackWithin: mpullbackWithin (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') f V s = pullbackWithin 𝕜 f V s.

Русский

Связь через равенство вытягиваний в эуклидовом случае: mpullbackWithin (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') f V s = pullbackWithin 𝕜 f V s.

LaTeX

$$$$ \mathrm{mpullbackWithin}\ (modelWithCornersSelf\ 𝕜\ E) (modelWithCornersSelf\ 𝕜\ E') f V s = \mathrm{pullbackWithin}\ 𝕜 f V s $$$$

Lean4

theorem mpullbackWithin_id {V : Π (x : M), TangentSpace I x} (h : UniqueMDiffWithinAt I s x) :
    mpullbackWithin I I id V s x = V x := by simp [mpullbackWithin_apply, mfderivWithin_id h]

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