toDirectLimit_tmul_of — Mathlib

English

The image of a simple tensor under the direct-limit lift equals the canonical simple tensor in the direct-limit target.

Русский

Образ простого тензора при лифте по прямому пределу равен каноническому простому тензору в целевом пределе.

LaTeX

$$$\bigl(\mathrm{toDirectLimit}\, f\, M\bigr)(\mathrm{of}\ i\ g \otimes m) = \mathrm{of}\ i (g \otimes m)$$$

Lean4

@[simp]
theorem toDirectLimit_tmul_of {i : ι} (g : G i) (m : M) :
    (toDirectLimit f M <| (of _ _ G f i g) ⊗ₜ m) = (of _ _ _ _ i (g ⊗ₜ m)) :=
  by
  rw [toDirectLimit, lift.tmul, lift_of]
  rfl

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