span_eq_span

Mathlib.LinearAlgebra.Span.Defs

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

English

For a suitable SetLike S M, span of s equals s as sets: (span R (s)) = s.

Русский

Для подходящей структуры S M множество span R s совпадает с s как множество.

LaTeX

$$$ (\operatorname{span} R (s : Set M)) = s. $$$

Lean4

theorem span_eq_span (hs : s ⊆ span R t) (ht : t ⊆ span R s) : span R s = span R t :=
  le_antisymm (span_le.2 hs) (span_le.2 ht)

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

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

Разделы

Аффилиация

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