feat(linear_algebra/span): add finite_span_is_compact_element (#13901)

This PR adds `finite_span_is_compact_element`, which extends `singleton_span_is_compact_element` to the spans of finite subsets.
This will be useful e.g. when proving the existence of a maximal submodule of a finitely generated module.

src/linear_algebra/span.lean

@@ -557,6 +557,22 @@ begin
   exact ⟨y, ⟨hyd, by simpa only [span_le, singleton_subset_iff]⟩⟩,
 end
 
+/-- The span of a finite subset is compact in the lattice of submodules. -/
+lemma finset_span_is_compact_element (S : finset M) :
+  complete_lattice.is_compact_element (span R S : submodule R M) :=
+begin
+  rw span_eq_supr_of_singleton_spans,
+  simp only [finset.mem_coe],
+  rw ←finset.sup_eq_supr,
+  exact complete_lattice.finset_sup_compact_of_compact S
+    (λ x _, singleton_span_is_compact_element x),
+end
+
+/-- The span of a finite subset is compact in the lattice of submodules. -/
+lemma finite_span_is_compact_element (S : set M) (h : S.finite) :
+  complete_lattice.is_compact_element (span R S : submodule R M) :=
+finite.coe_to_finset h ▸ (finset_span_is_compact_element h.to_finset)
+
 instance : is_compactly_generated (submodule R M) :=
 ⟨λ s, ⟨(λ x, span R {x}) '' s, ⟨λ t ht, begin
   rcases (set.mem_image _ _ _).1 ht with ⟨x, hx, rfl⟩,