finrank_eq_zero_of_not_exists_basis_finite

English

If there is no finite-basis indexed by any Finset of M, then finrank_R(M) = 0.

Русский

Если не существует базы, индексируемой по любому конечному подмножеству M, то finrank_R(M) = 0.

LaTeX

$$$$ \\lnot \\exists s : Finset M, \\text{Nonempty}(\\text{Basis}(s, R, M)) \\\\Rightarrow \\\\operatorname{finrank}_R M = 0.$$$$

Lean4

theorem finrank_eq_zero_of_not_exists_basis_finite (h : ¬∃ (s : Set M) (_ : Basis.{v} (s : Set M) R M), s.Finite) :
    finrank R M = 0 :=
  finrank_eq_zero_of_basis_imp_not_finite fun s b hs => h ⟨s, b, hs⟩

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