feat(measure_theory/borel_space): the inverse of a closed embedding i…

…s measurable (#5567)

Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>

src/data/set/function.lean

@@ -539,6 +539,25 @@ begin
     exact hfs'.surj_on.mono hs' (subset.refl _) }
 end
 
+lemma preimage_inv_fun_of_mem [n : nonempty α] {f : α → β} (hf : injective f) {s : set α}
+  (h : classical.choice n ∈ s) : inv_fun f ⁻¹' s = f '' s ∪ (range f)ᶜ :=
+begin
+  ext x,
+  rcases em (x ∈ range f) with ⟨a, rfl⟩|hx,
+  { simp [left_inverse_inv_fun hf _, mem_image_of_injective hf] },
+  { simp [mem_preimage, inv_fun_neg hx, h, hx] }
+end
+
+lemma preimage_inv_fun_of_not_mem [n : nonempty α] {f : α → β} (hf : injective f)
+  {s : set α} (h : classical.choice n ∉ s) : inv_fun f ⁻¹' s = f '' s :=
+begin
+  ext x,
+  rcases em (x ∈ range f) with ⟨a, rfl⟩|hx,
+  { rw [mem_preimage, left_inverse_inv_fun hf, mem_image_of_injective hf] },
+  { have : x ∉ f '' s, from λ h', hx (image_subset_range _ _ h'),
+    simp only [mem_preimage, inv_fun_neg hx, h, this] },
+end
+
 end set
 
 /-! ### Piecewise defined function -/

src/measure_theory/borel_space.lean

@@ -523,6 +523,18 @@ lemma measurable.sub [add_group α] [topological_add_group α] [second_countable
   measurable (λ x, f x - g x) :=
 by simpa only [sub_eq_add_neg] using hf.add hg.neg
 
+lemma closed_embedding.measurable_inv_fun [n : nonempty β] {g : β → γ} (hg : closed_embedding g) :
+  measurable (function.inv_fun g) :=
+begin
+  refine measurable_of_is_closed (λ s hs, _),
+  by_cases h : classical.choice n ∈ s,
+  { rw preimage_inv_fun_of_mem hg.to_embedding.inj h,
+    exact (hg.closed_iff_image_closed.mp hs).is_measurable.union
+      hg.closed_range.is_measurable.compl },
+  { rw preimage_inv_fun_of_not_mem hg.to_embedding.inj h,
+    exact (hg.closed_iff_image_closed.mp hs).is_measurable }
+end
+
 lemma measurable_comp_iff_of_closed_embedding {f : δ → β} (g : β → γ) (hg : closed_embedding g) :
   measurable (g ∘ f) ↔ measurable f :=
 begin