English
For any vector space V over a field K with aleph0 ≤ dim_K V, the lifted rank of V is strictly less than the rank of the dual space, i.e. lift(rank_K V) < rank_K(V*) where V* = Hom_K(V,K).
Русский
Для любого пространства V над полем K с aleph0 ≤ dim_K V подъем ранга V меньше ранга двойственного пространства, то есть lift(rank_K V) < rank_K(V*), где V* = Hom_K(V,K).
LaTeX
$$$\operatorname{lift}(\operatorname{rank}_K V) < \operatorname{rank}_{K}(V^*).$$$
Lean4
theorem lift_rank_lt_rank_dual {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V]
(h : ℵ₀ ≤ Module.rank K V) : Cardinal.lift.{u} (Module.rank K V) < Module.rank K (V →ₗ[K] K) :=
by
rw [rank_dual_eq_card_dual_of_aleph0_le_rank h, ← rank_dual_eq_card_dual_of_aleph0_le_rank' h]
exact lift_rank_lt_rank_dual' h
