injective_pi_lapply

Mathlib.LinearAlgebra.DFinsupp

URI: https://scilib.ai/kg/mathlib#DFinsupp.injective_pi_lapply

English

Reiterating injectivity of linear maps described by coordinate projections.

Русский

Инъективность отображения, задаваемого через проекции координат.

LaTeX

$$$\\text{injective }(\\mathrm{LinearMap.pi}\\;\\mathrm{lapply})$$$

Lean4

theorem injective_pi_lapply : Function.Injective (LinearMap.pi (R := R) <| lapply (M := M)) := fun _ _ h ↦
  ext fun _ ↦ congr_fun h _

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru