span_mono

Mathlib.LinearAlgebra.Span.Defs

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

English

The span operator is monotone with respect to inclusion.

Русский

Оператор span монотонен относительно включения.

LaTeX

$$$ s \subseteq t \Rightarrow \operatorname{span} R s \le \operatorname{span} R t. $$$

Lean4

@[gcongr]
theorem span_mono (h : s ⊆ t) : span R s ≤ span R t :=
  span_le.2 <| Subset.trans h subset_span

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

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

Разделы

Аффилиация

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