setFinite — Mathlib

English

Let M be a finite R-module. If b is a subset of M which is linearly independent, then b is a finite set.

Русский

Пусть M — конечномерный модуль над R. Пусть b ⊆ M и b линейно независимо. Тогда b конечно.

LaTeX

$$$\text{Module.Finite } R M \;\land\; \text{LinearIndependent } R (\lambda x: (x:M)) \;\Rightarrow\; b.Finite$$$

Lean4

theorem setFinite [Module.Finite R M] {b : Set M} (h : LinearIndependent R fun x : b => (x : M)) : b.Finite :=
  Cardinal.lt_aleph0_iff_set_finite.mp h.lt_aleph0_of_finite

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