K : Type u
V : Type v
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
s t : Submodule K V
inst✝¹ : FiniteDimensional K { x // x ∈ s }
inst✝ : FiniteDimensional K { x // x ∈ t }
⊢ finrank K { x // x ∈ s ⊔ t } ≤ finrank K { x // x ∈ s ⊔ t } + finrank K { x // x ∈ s ⊓ t }
K : Type u
V : Type v
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
s t : Submodule K V
inst✝¹ : FiniteDimensional K { x // x ∈ s }
inst✝ : FiniteDimensional K { x // x ∈ t }
⊢ finrank K { x // x ∈ s ⊔ t } ≤ finrank K { x // x ∈ s } + finrank K { x // x ∈ t }
rw [← finrank_sup_add_finrank_inf_eq]
no goals
K : Type u
V : Type v
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
s t : Submodule K V
inst✝¹ : FiniteDimensional K { x // x ∈ s }
inst✝ : FiniteDimensional K { x // x ∈ t }
⊢ finrank K { x // x ∈ s ⊔ t } ≤ finrank K { x // x ∈ s ⊔ t } + finrank K { x // x ∈ s ⊓ t }
exact self_le_add_right _ _