feat(measure_theory): prove that more functions are measurable (#4266)

Mostly additions to `borel_space`.
Generalize `measurable_bsupr` and `measurable_binfi` to countable sets (instead of encodable underlying types). Use the lemma `countable_encodable` to get the original behavior.
Some cleanup in `borel_space`: more instances are in `variables`, and lemmas with the same instances a bit more.
One downside: there is a big import bump in `borel_space`, it currently imports `hahn_banach`. This is (only) used in `measurable_smul_const`. If someone has a proof sketch (in math) of `measurable_smul_const` that doesn't involve Hahn Banach (and that maybe generalizes `real` to a topological field or something), please let me know.

src/analysis/normed_space/finite_dimension.lean

@@ -326,6 +326,26 @@ lemma continuous_linear_map.exists_right_inverse_of_surjective [finite_dimension
 let ⟨g, hg⟩ := (f : E →ₗ[𝕜] F).exists_right_inverse_of_surjective hf in
 ⟨g.to_continuous_linear_map, continuous_linear_map.ext $ linear_map.ext_iff.1 hg⟩
 
+lemma closed_embedding_smul_left {c : E} (hc : c ≠ 0) : closed_embedding (λ x : 𝕜, x • c) :=
+begin
+  haveI : finite_dimensional 𝕜 (submodule.span 𝕜 {c}) :=
+    finite_dimensional.span_of_finite 𝕜 (finite_singleton c),
+  have m1 : closed_embedding (coe : submodule.span 𝕜 {c} → E) :=
+  (submodule.span 𝕜 {c}).closed_of_finite_dimensional.closed_embedding_subtype_coe,
+  have m2 : closed_embedding
+    (linear_equiv.to_span_nonzero_singleton 𝕜 E c hc : 𝕜 → submodule.span 𝕜 {c}) :=
+  (continuous_linear_equiv.to_span_nonzero_singleton 𝕜 c hc).to_homeomorph.closed_embedding,
+  exact m1.comp m2
+end
+
+/- `smul` is a closed map in the first argument. -/
+lemma is_closed_map_smul_left (c : E) : is_closed_map (λ x : 𝕜, x • c) :=
+begin
+  by_cases hc : c = 0,
+  { simp_rw [hc, smul_zero], exact is_closed_map_const },
+  { exact (closed_embedding_smul_left hc).is_closed_map }
+end
+
 end complete_field
 
 section proper_field

src/linear_algebra/basic.lean

@@ -2096,22 +2096,24 @@ section
 noncomputable theory
 open_locale classical
 
+lemma ker_to_span_singleton {x : M} (h : x ≠ 0) : (to_span_singleton K M x).ker = ⊥ :=
+begin
+  ext c, split,
+  { intros hc, rw submodule.mem_bot, rw mem_ker at hc, by_contra hc',
+    have : x = 0,
+      calc x = c⁻¹ • (c • x) : by rw [← mul_smul, inv_mul_cancel hc', one_smul]
+      ... = c⁻¹ • ((to_span_singleton K M x) c) : rfl
+      ... = 0 : by rw [hc, smul_zero],
+    tauto },
+  { rw [mem_ker, submodule.mem_bot], intros h, rw h, simp }
+end
+
 /-- Given a nonzero element `x` of a vector space `M` over a field `K`, the natural
     map from `K` to the span of `x`, with invertibility check to consider it as an
     isomorphism.-/
 def to_span_nonzero_singleton (x : M) (h : x ≠ 0) : K ≃ₗ[K] (submodule.span K ({x} : set M)) :=
 linear_equiv.trans
-  ( linear_equiv.of_injective (to_span_singleton K M x)
-    begin
-      ext c, split,
-      { intros hc, rw submodule.mem_bot, rw mem_ker at hc, by_contra hc',
-        have : x = 0,
-          calc x = c⁻¹ • (c • x) : by rw [← mul_smul, inv_mul_cancel hc', one_smul]
-          ... = c⁻¹ • ((to_span_singleton K M x) c) : rfl
-          ... = 0 : by rw [hc, smul_zero],
-        tauto },
-      { rw [mem_ker, submodule.mem_bot], intros h, rw h, simp }
-    end )
+  (linear_equiv.of_injective (to_span_singleton K M x) (ker_to_span_singleton K M h))
   (of_eq (to_span_singleton K M x).range (submodule.span K {x}) (span_singleton_eq_range K M x).symm)
 
 lemma to_span_nonzero_singleton_one (x : M) (h : x ≠ 0) : to_span_nonzero_singleton K M x h 1