finite_ne_bot_of_iSupIndep — Mathlib

English

For any family N: ι → Submodule R M that is iSupIndep, the set of indices i for which N(i) is nontrivial is finite.

Русский

Для любой семейства N: ι → Подпространство R M, которое является iSupIndep, множество индексов i, для которых N(i) не тривиально, конечно.

LaTeX

$$$\lbrace i \in ι \mid N(i) \neq \bot \rbrace$ имеет конечную кардинальность$$

Lean4

theorem finite_ne_bot_of_iSupIndep {ι : Type*} {N : ι → Submodule R M} (h : iSupIndep N) : Set.Finite {i | N i ≠ ⊥} :=
  WellFoundedGT.finite_ne_bot_of_iSupIndep h

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