vectorSpan_mono

Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs

URI: https://scilib.ai/kg/mathlib#vectorSpan_mono

← MathLib Explorer

English

If s1 ⊆ s2 then vectorSpan k s1 ≤ vectorSpan k s2.

Русский

Если s1 ⊆ s2, то vectorSpan k s1 ≤ vectorSpan k s2.

LaTeX

$$$ \\text{If } s_1 \\subseteq s_2, \\quad vectorSpan\\ k\\ s_1 \\le vectorSpan\\ k\\ s_2 $$$

Lean4

/-- `vectorSpan` is monotone. -/
theorem vectorSpan_mono {s₁ s₂ : Set P} (h : s₁ ⊆ s₂) : vectorSpan k s₁ ≤ vectorSpan k s₂ :=
  Submodule.span_mono (vsub_self_mono h)

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

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

Разделы

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

Аффилиация

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