English
If V is an infinite-dimensional vector space over a field K, then the dimension of the lifted rank of V is strictly less than the dimension of the dual space V* (with respect to Kᵒᵖ). In particular, dim_Kᵒᵖ(V*) is strictly larger than lift(dim_K V).
Русский
Если размерность V бесконечна над полем K, то подъем размерности V строго меньше размерности двойственного пространства V*, когда рассматривается соответствующая структура над Kᵒᵖ.
LaTeX
$$$\operatorname{lift}(\operatorname{rank}_K V) < \operatorname{rank}_{K^{\mathrm{op}}}(V \to_K K),$$$
Lean4
theorem lift_rank_lt_rank_dual' {V : Type v} [AddCommGroup V] [Module K V] (h : ℵ₀ ≤ Module.rank K V) :
Cardinal.lift.{u} (Module.rank K V) < Module.rank Kᵐᵒᵖ (V →ₗ[K] K) :=
by
obtain ⟨⟨ι, b⟩⟩ := Module.Free.exists_basis (R := K) (M := V)
rw [← b.mk_eq_rank'', rank_dual_eq_card_dual_of_aleph0_le_rank' h, ← (b.constr ℕ (M' := K)).toEquiv.cardinal_eq,
mk_arrow]
apply cantor'
erw [nat_lt_lift_iff, one_lt_iff_nontrivial]
infer_instance
