comapDomain'_smul — Mathlib

English

A variant with a left inverse h' of h satisfies comapDomain' h hh' (r • f) = r • comapDomain' h hh' f.

Русский

Вариант с левой обратной функцией h' к h: comapDomain' h hh' (r • f) = r • comapDomain' h hh' f.

LaTeX

$$$$ \\mathrm{comapDomain'}\\, h\\, hh'\\big( r \\cdot f \\big) = r \\cdot \\mathrm{comapDomain'}\\, h\\, hh'\\, f $$$$

Lean4

@[simp]
theorem comapDomain'_smul [∀ i, Zero (β i)] [∀ i, SMulZeroClass γ (β i)] (h : κ → ι) {h' : ι → κ}
    (hh' : Function.LeftInverse h' h) (r : γ) (f : Π₀ i, β i) : comapDomain' h hh' (r • f) = r • comapDomain' h hh' f :=
  by
  ext
  rw [smul_apply, comapDomain'_apply, smul_apply, comapDomain'_apply]

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