mpullback_add_apply — Mathlib

English

The mpullbackWithin for modelWithCorners equals the standard pullbackWithin: mpullbackWithin 𝓘(𝕜, E) 𝓘(𝕜, E') f V s = pullbackWithin 𝕜 f V s.

Русский

Для общей модели разности mpullbackWithin совпадает с обычным pullbackWithin: mpullbackWithin 𝓘(𝕜, E) 𝓘(𝕜, E') f V s = pullbackWithin 𝕜 f V s.

LaTeX

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

Lean4

theorem mpullback_add_apply : mpullback I I' f (V + V₁) x = mpullback I I' f V x + mpullback I I' f V₁ x := by
  simp [mpullback_apply]

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