finrank_le_finrank_of_rank_le_rank

English

If the rank of M is bounded by the lift of the rank of N and the rank of N is finite, then finrank_R M ≤ finrank_R N.

Русский

Если ранг M ограничен лефтом ранга N и ранг N конечен, то finrank_R M ≤ finrank_R N.

LaTeX

$$$\\bigl( \\operatorname{lift} \\bigl( \\operatorname{rank}_R M \\bigr) \\le \\operatorname{lift} \\bigl( \\operatorname{rank}_R N \\bigr) \\bigr) \\land\\bigl( \\operatorname{rank}_R N < \\aleph_0 \\bigr) \\Rightarrow \\mathrm{finrank}_R M \\le \\mathrm{finrank}_R N$$$

Lean4

theorem finrank_le_finrank_of_rank_le_rank (h : lift.{w} (Module.rank R M) ≤ Cardinal.lift.{v} (Module.rank R N))
    (h' : Module.rank R N < ℵ₀) : finrank R M ≤ finrank R N := by
  simpa only [toNat_lift] using toNat_le_toNat h (lift_lt_aleph0.mpr h')

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