spanFinrank_span_le_encard

Mathlib.Algebra.Module.SpanRank

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

← MathLib Explorer

English

The finite rank of span s is at most the encard of s.

Русский

Конечная ранга span s не превосходит encard s.

LaTeX

$$$(\operatorname{span} R s).spanFinrank.cast \\le s.encard$$$

Lean4

theorem spanFinrank_span_le_encard (s : Set M) : (span R s).spanFinrank ≤ s.encard :=
  by
  rw [spanFinrank, Set.encard, ENat.card]
  exact le_trans (by simp) ((toENat).monotone' (spanRank_span_le_card (R := R) s))

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

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

Разделы

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

Аффилиация

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