rank_span_of_finset

Mathlib.LinearAlgebra.Dimension.Constructions

URI: https://scilib.ai/kg/mathlib#rank_span_of_finset

English

The rank of span of a Finset is finite (less than aleph_0).

Русский

Ранг пространства, образуемого span от Finset, конечно конечен (<aleph_0).

LaTeX

$$$ \\operatorname{Module.rank} R (\\operatorname{span}_R (s : Set M)) < \\aleph_0. $$$

Lean4

theorem rank_span_of_finset (s : Finset M) : Module.rank R (span R (s : Set M)) < ℵ₀ :=
  (rank_span_finset_le s).trans_lt (Cardinal.nat_lt_aleph0 _)

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

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

Разделы

Аффилиация

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