injOn

Mathlib.LinearAlgebra.LinearIndependent.Defs

URI: https://scilib.ai/kg/mathlib#LinearIndepOn.injOn

English

If the subfamily on s is LI, then v is injective on s.

Русский

Если подсемейство на s линейно независимо, то отображение v ограничено на s инъективно.

LaTeX

$$$\\operatorname{LinearIndepOn}(R,v,s) \\Rightarrow \\operatorname{InjOn}(v,s)$$$

Lean4

theorem injOn [Nontrivial R] (hv : LinearIndepOn R v s) : InjOn v s :=
  injOn_iff_injective.2 <| LinearIndependent.injective hv

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

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

Разделы

Аффилиация

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