spanRank_span_le_card

Mathlib.Algebra.Module.SpanRank

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

← MathLib Explorer

English

For any subset s, the rank of span R s is at most the cardinality of s.

Русский

Для любого подмножества s ранг span R s не больше мощности s.

LaTeX

$$$\operatorname{spanRank}(\operatorname{span} R s) \le |s|$$$

Lean4

theorem spanRank_span_le_card (s : Set M) : (Submodule.span R s).spanRank ≤ #s :=
  by
  rw [spanRank]
  let s' : { s1 : Set M // span R s1 = span R s } := ⟨s, rfl⟩
  exact ciInf_le' _ s'

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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