feat(linear_algebra/finite_dimensional): dim_add_le_dim_add_dim (#16301)

Add a `finrank` version of a lemma that already exists for
`module.rank`.  The proof is exactly the same as the proof of the
`module.rank` version, and, as with the previous
`dim_sup_add_dim_inf_eq` lemma that it uses, so is the name (but in
the `submodule` namespace in the case of the `finrank` versions).

Author: jsm28

src/linear_algebra/finite_dimensional.lean

@@ -861,6 +861,11 @@ begin
   exact key
 end
 
+lemma dim_add_le_dim_add_dim (s t : submodule K V)
+  [finite_dimensional K s] [finite_dimensional K t] :
+  finrank K (s ⊔ t : submodule K V) ≤ finrank K s + finrank K t :=
+by { rw [← dim_sup_add_dim_inf_eq], exact self_le_add_right _ _ }
+
 lemma eq_top_of_disjoint [finite_dimensional K V] (s t : submodule K V)
   (hdim : finrank K s + finrank K t = finrank K V)
   (hdisjoint : disjoint s t) : s ⊔ t = ⊤ :=