span_smul_le

Mathlib.LinearAlgebra.Span.Defs

URI: https://scilib.ai/kg/mathlib#Submodule.span_smul_le

← MathLib Explorer

English

If U ⊆ span V and V ⊆ span W, then U ⊆ span W.

Русский

Если U ⊆ span V и V ⊆ span W, тогда U ⊆ span W.

LaTeX

$$$$ U \subseteq \operatorname{span} R V \;\to\; V \subseteq \operatorname{span} R W \;\Rightarrow\; U \subseteq \operatorname{span} R W $$$$

Lean4

theorem span_smul_le (s : Set M) (r : R) : span R (r • s) ≤ span R s :=
  by
  rw [span_le]
  rintro _ ⟨x, hx, rfl⟩
  exact smul_mem (span R s) r (subset_span hx)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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