cardinal_lift_le_rank — Mathlib

English

If a linearly independent family v: ι → M exists, then the lifted cardinal of ι does not exceed the lifted rank of M.

Русский

Если существует линейно независимая семейство v: ι → M, то подъем кардинала ι не превосходит подъема ранга M.

LaTeX

$$$\operatorname{lift}(\#\iota) \le \operatorname{lift}(\operatorname{rank}_R(M))$$$

Lean4

theorem cardinal_lift_le_rank {ι : Type w} {v : ι → M} (hv : LinearIndependent R v) :
    Cardinal.lift.{v} #ι ≤ Cardinal.lift.{w} (Module.rank R M) :=
  by
  rw [Module.rank]
  refine le_trans ?_ (lift_le.mpr <| le_ciSup (bddAbove_range _) ⟨_, hv.linearIndepOn_id⟩)
  exact lift_mk_le'.mpr ⟨(Equiv.ofInjective _ hv.injective).toEmbedding⟩

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