closure_le_toAddSubmonoid_span

Mathlib.LinearAlgebra.Span.Defs

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

English

The AddSubmonoid closure of s is contained in the AddSubmonoid of the span of s.

Русский

Замыкание AddSubmonoid множества s содержится в AddSubmonoid порожденного Span(s).

LaTeX

$$$ AddSubmonoid.closure s \le (\operatorname{span} R s).toAddSubmonoid. $$$

Lean4

theorem closure_le_toAddSubmonoid_span {s : Set M} : AddSubmonoid.closure s ≤ (span R s).toAddSubmonoid :=
  closure_subset_span

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

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

Разделы

Аффилиация

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