lsetToSet — Mathlib

English

The inverse of the linear equivalence sends Pi.single i m to lof i m.

Русский

Обратное линейного эквивалентного отображения отправляет Pi.single i m в lof i m.

LaTeX

$$$ (linearEquivFunOnFintype\\; R\\; ι\\; M)^{-1} (\\Pi.single\\; i\\; m) = \\mathrm{lof}\\; R\\; ι\\; M\\; i\\; m $$$

Lean4

/-- The inclusion of a subset of the direct summands
into a larger subset of the direct summands, as a linear map. -/
def lsetToSet (S T : Set ι) (H : S ⊆ T) : (⨁ i : S, M i) →ₗ[R] ⨁ i : T, M i :=
  toModule R _ _ fun i ↦ lof R T (fun i : Subtype T ↦ M i) ⟨i, H i.prop⟩

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