subset_span

Mathlib.RingTheory.Ideal.Span

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

English

Every set is contained in its span: s ⊆ span(s).

Русский

Каждое множество содержится в своем порождении: s ⊆ span(s).

LaTeX

$$$s \\subseteq \\operatorname{span}(s)$$$

Lean4

theorem subset_span {s : Set α} : s ⊆ span s :=
  Submodule.subset_span

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

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

Разделы

Аффилиация

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