comapDomain_smul — Mathlib

English

Composing with comapDomain and then scaling equals scaling then comapping: comapDomain h hh (r • f) = r • comapDomain h hh f.

Русский

Сочетание comapDomain и масштабирования эквивалентно масштабированию после применения comapDomain: 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 : κ → ι) (hh : Function.Injective 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]

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