comapDomain_add — Mathlib

English

comapDomain distributes over addition: comapDomain h hh (f + g) = comapDomain h hh f + comapDomain h hh g.

Русский

comapDomain по сложению: 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 : κ → ι) (hh : Function.Injective 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]

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