fintypeNeBotOfFiniteDimensional — Mathlib

English

A nontrivial independent family over a finite-dimensional module yields a finite type of nonzero components.

Русский

Независимая семейство над конечномерным модулем даёт конечный тип ненулевых компонент.

LaTeX

$$Неcomputable defin: \text{Fintype }\{ i : ι \;\vert\; p(i) \neq \bot \} for iSupIndep p$$

Lean4

/-- If `p` is an independent family of submodules of a `R`-finite module `M`, then the
number of nontrivial subspaces in the family `p` is finite. -/
noncomputable def fintypeNeBotOfFiniteDimensional {p : ι → Submodule R M} (hp : iSupIndep p) :
    Fintype { i : ι // p i ≠ ⊥ } :=
  by
  suffices #{ i // p i ≠ ⊥ } < (ℵ₀ : Cardinal.{w})
    by
    rw [Cardinal.lt_aleph0_iff_fintype] at this
    exact this.some
  refine lt_of_le_of_lt hp.subtype_ne_bot_le_finrank_aux ?_
  simp [Cardinal.nat_lt_aleph0]

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