rank_lt_rank_dual' — Mathlib

English

If aleph0 ≤ dim_K V, then the dimension of V is strictly less than the dimension of the dual V* (unlifted version).

Русский

Если ℵ0 ≤ dim_K V, то размерность V строго меньше размерности двойственного пространства V* (без подъемов).

LaTeX

$$$\aleph_0 \le \operatorname{rank}_K V \Rightarrow \operatorname{rank}_K V < \operatorname{rank}_K(V^*).$$$

Lean4

theorem rank_lt_rank_dual' {V : Type u} [AddCommGroup V] [Module K V] (h : ℵ₀ ≤ Module.rank K V) :
    Module.rank K V < Module.rank Kᵐᵒᵖ (V →ₗ[K] K) := by convert lift_rank_lt_rank_dual' h; rw [lift_id]

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