mpullbackWithin_add_apply — Mathlib

English

mpullbackWithin I I' f (V + V1) s x = mpullbackWithin I I' f V s x + mpullbackWithin I I' f V1 s x.

Русский

mpullbackWithin I I' f (V + V1) s x = mpullbackWithin I I' f V s x + mpullbackWithin I I' f V1 s x.

LaTeX

$$$$ \mathrm{mpullbackWithin}\ I\ I'\ f\ (V + V1)\ s\ x = \mathrm{mpullbackWithin}\ I\ I'\ f\ V\ s\ x + \mathrm{mpullbackWithin}\ I\ I'\ f\ V1\ s\ x $$$$

Lean4

theorem mpullbackWithin_add_apply :
    mpullbackWithin I I' f (V + V₁) s x = mpullbackWithin I I' f V s x + mpullbackWithin I I' f V₁ s x := by
  simp [mpullbackWithin_apply]

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