kroneckerMap_map — Mathlib

English

Applying a map g on the output of kroneckerMap is the same as kroneckerMap with the composed function g ∘ f.

Русский

Применение отображения g к результату kroneckerMap эквивалентно kroneckerMap с композиции g ∘ f.

LaTeX

$$$\\forall {\\alpha} {\\beta} {\\gamma} {\\gamma'} {l} {m} {n} {p} (f : \u03b1 \u2192 \u03b2 \u2192 \u0393) (g : \u0393 \u2192 \u0393') (A : Matrix l m \u03b1) (B : Matrix n p \u03b2), (kroneckerMap f A B).map g = kroneckerMap (\\u03bb a b, g (f a b)) A B$$$

Lean4

theorem kroneckerMap_map (f : α → β → γ) (g : γ → γ') (A : Matrix l m α) (B : Matrix n p β) :
    (kroneckerMap f A B).map g = kroneckerMap (fun a b => g (f a b)) A B :=
  ext fun _ _ => rfl

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