span_le

Mathlib.LinearAlgebra.Span.Defs

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

English

If s ⊆ t, then span R s ≤ span R t.

Русский

Если s ⊆ t, тогда span_R s ⊆ span_R t.

LaTeX

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

Lean4

theorem span_le {p} : span R s ≤ p ↔ s ⊆ p :=
  ⟨Subset.trans subset_span, fun ss _ h => mem_span.1 h _ ss⟩

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

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

Разделы

Аффилиация

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