subset_span

Mathlib.LinearAlgebra.Span.Defs

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

English

Any set s is contained in its span: s ⊆ span R s.

Русский

Любое множество s содержится в своей линейной оболочке: s ⊆ span_R s.

LaTeX

$$$ s \subseteq \operatorname{span} R s. $$$

Lean4

@[simp, aesop safe 20 (rule_sets := [SetLike])]
theorem subset_span : s ⊆ span R s := fun _ h => mem_span.2 fun _ hp => hp h

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

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

Разделы

Аффилиация

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