K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
ι : Type w
inf : Infinite ι
inst✝ : FiniteDimensional K V
v : ι → V
h_lin_indep : LinearIndependent K v
⊢ False
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
ι : Type w
inf : Infinite ι
inst✝ : FiniteDimensional K V
v : ι → V
⊢ ¬LinearIndependent K v
intro h_lin_indep
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
ι : Type w
inf : Infinite ι
inst✝ : FiniteDimensional K V
v : ι → V
h_lin_indep : LinearIndependent K v
this : ¬ℵ₀ ≤ (#ι)
⊢ False
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
ι : Type w
inf : Infinite ι
inst✝ : FiniteDimensional K V
v : ι → V
h_lin_indep : LinearIndependent K v
⊢ False
have : ¬ℵ₀ ≤ (#ι) := not_le.mpr (lt_aleph0_of_linearIndependent h_lin_indep)
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
ι : Type w
inf : Infinite ι
inst✝ : FiniteDimensional K V
v : ι → V
h_lin_indep : LinearIndependent K v
this✝ : ¬ℵ₀ ≤ (#ι)
this : ℵ₀ ≤ (#ι)
⊢ False
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
ι : Type w
inf : Infinite ι
inst✝ : FiniteDimensional K V
v : ι → V
h_lin_indep : LinearIndependent K v
this : ¬ℵ₀ ≤ (#ι)
⊢ False
have : ℵ₀ ≤ (#ι) := infinite_iff.mp inf
no goals
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
ι : Type w
inf : Infinite ι
inst✝ : FiniteDimensional K V
v : ι → V
h_lin_indep : LinearIndependent K v
this✝ : ¬ℵ₀ ≤ (#ι)
this : ℵ₀ ≤ (#ι)
⊢ False
contradiction