English
If IsReflexive over a field K, then the vector space is finite-dimensional.
Русский
Если векторное пространство над полем K рефлексивно, то оно конечно размерно.
LaTeX
$$FiniteDimensional_K(V)$$
Lean4
instance instFiniteDimensionalOfIsReflexive (K V : Type*) [Field K] [AddCommGroup V] [Module K V] [IsReflexive K V] :
FiniteDimensional K V := by
rw [FiniteDimensional, ← rank_lt_aleph0_iff]
by_contra! contra
suffices lift (Module.rank K V) < Module.rank K (Dual K (Dual K V))
by
have heq :=
lift_rank_eq_of_equiv_equiv (R := K) (R' := K) (M := V) (M' := Dual K (Dual K V)) (ZeroHom.id K) (evalEquiv K V)
bijective_id (fun r v ↦ (evalEquiv K V).map_smul _ _)
rw [← lift_umax, heq, lift_id'] at this
exact lt_irrefl _ this
have h₁ : lift (Module.rank K V) < Module.rank K (Dual K V) := lift_rank_lt_rank_dual contra
have h₂ : Module.rank K (Dual K V) < Module.rank K (Dual K (Dual K V)) :=
by
convert lift_rank_lt_rank_dual <| le_trans (by simpa) h₁.le
rw [lift_id']
exact lt_trans h₁ h₂
