mono

Mathlib.LinearAlgebra.LinearIndependent.Defs

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

English

If hv: LinearIndepOn R v s and t ⊆ s, then LinearIndepOn R v t.

Русский

Если hv: LinearIndepOn R v s и t ⊆ s, то LinearIndepOn R v t.

LaTeX

$$$\\operatorname{LinearIndepOn}(R,v,s) \\to \\operatorname{LinearIndepOn}(R,v,t)$ при $t\\subseteq s$$$

Lean4

theorem mono {t s : Set ι} (hs : LinearIndepOn R v s) (h : t ⊆ s) : LinearIndepOn R v t :=
  hs.comp _ <| Set.inclusion_injective h

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

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

Разделы

Аффилиация

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