comapDomain'_add — Mathlib

English

comapDomain' h hh' (f + g) = comapDomain' h hh' f + comapDomain' h hh' g.

Русский

comapDomain' h hh' (f+g) = comapDomain' h hh' f + comapDomain' h hh' g.

LaTeX

$$$\\mathrm{comapDomain'}(h,hh')(f+g) = \\mathrm{comapDomain'}(h,hh')f + \\mathrm{comapDomain'}(h,hh')g$$$

Lean4

@[simp]
theorem comapDomain'_add [∀ i, AddZeroClass (β i)] (h : κ → ι) {h' : ι → κ} (hh' : Function.LeftInverse h' h)
    (f g : Π₀ i, β i) : comapDomain' h hh' (f + g) = comapDomain' h hh' f + comapDomain' h hh' g :=
  by
  ext
  rw [add_apply, comapDomain'_apply, comapDomain'_apply, comapDomain'_apply, add_apply]

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