[Merged by Bors] - feat(measurable_space): more properties of measurable sets in a product

src/data/set/lattice.lean

@@ -551,11 +551,11 @@ instance : complete_boolean_algebra (set α) :=
   .. set.boolean_algebra, .. set.lattice_set }
 
 lemma sInter_union_sInter {S T : set (set α)} :
-  (⋂₀S) ∪ (⋂₀T) = (⋂p ∈ set.prod S T, (p : (set α) × (set α)).1 ∪ p.2) :=
+  (⋂₀S) ∪ (⋂₀T) = (⋂p ∈ S.prod T, (p : (set α) × (set α)).1 ∪ p.2) :=
 Inf_sup_Inf
 
 lemma sUnion_inter_sUnion {s t : set (set α)} :
-  (⋃₀s) ∩ (⋃₀t) = (⋃p ∈ set.prod s t, (p : (set α) × (set α )).1 ∩ p.2) :=
+  (⋃₀s) ∩ (⋃₀t) = (⋃p ∈ s.prod t, (p : (set α) × (set α )).1 ∩ p.2) :=
 Sup_inf_Sup
 
 /-- If `S` is a set of sets, and each `s ∈ S` can be represented as an intersection
@@ -940,7 +940,7 @@ lemma image_seq {f : β → γ} {s : set (α → β)} {t : set α} :
   f '' seq s t = seq ((∘) f '' s) t :=
 by rw [← singleton_seq, ← singleton_seq, seq_seq, image_singleton]
 
-lemma prod_eq_seq {s : set α} {t : set β} : set.prod s t = (prod.mk '' s).seq t :=
+lemma prod_eq_seq {s : set α} {t : set β} : s.prod t = (prod.mk '' s).seq t :=
 begin
   ext ⟨a, b⟩,
   split,
@@ -950,12 +950,12 @@ end
 
 lemma prod_image_seq_comm (s : set α) (t : set β) :
   (prod.mk '' s).seq t = seq ((λb a, (a, b)) '' t) s :=
-by rw [← prod_eq_seq, ← image_swap_prod, prod_eq_seq, image_seq, ← image_comp]
+by rw [← prod_eq_seq, ← image_swap_prod, prod_eq_seq, image_seq, ← image_comp, prod.swap]
 
 end seq
 
 theorem monotone_prod [preorder α] {f : α → set β} {g : α → set γ}
-  (hf : monotone f) (hg : monotone g) : monotone (λx, set.prod (f x) (g x)) :=
+  (hf : monotone f) (hg : monotone g) : monotone (λx, (f x).prod (g x)) :=
 assume a b h, prod_mono (hf h) (hg h)
 
 instance : monad set :=

src/measure_theory/integration.lean

@@ -216,7 +216,7 @@ lemma pair_preimage (f : α →ₛ β) (g : α →ₛ γ) (s : set β) (t : set
 /- A special form of `pair_preimage` -/
 lemma pair_preimage_singleton (f : α →ₛ β) (g : α →ₛ γ) (b : β) (c : γ) :
   (pair f g) ⁻¹' {(b, c)} = (f ⁻¹' {b}) ∩ (g ⁻¹' {c}) :=
-by { rw ← prod_singleton_singleton, exact pair_preimage _ _ _ _ }
+by { rw ← singleton_prod_singleton, exact pair_preimage _ _ _ _ }
 
 theorem bind_const (f : α →ₛ β) : f.bind (const α) = f := by ext; simp
 

src/measure_theory/lebesgue_measure.lean

@@ -222,7 +222,7 @@ end
 
 The outer Lebesgue measure is the completion of this measure. (TODO: proof this)
 -/
-instance : measure_space ℝ :=
+instance real.measure_space : measure_space ℝ :=
 ⟨{to_outer_measure := lebesgue_outer,
   m_Union :=
     have borel ℝ ≤ lebesgue_outer.caratheodory,

src/measure_theory/measurable_space.lean

@@ -580,37 +580,52 @@ section prod
 instance [m₁ : measurable_space α] [m₂ : measurable_space β] : measurable_space (α × β) :=
 m₁.comap prod.fst ⊔ m₂.comap prod.snd
 
-lemma measurable_fst [measurable_space α] [measurable_space β] :
-  measurable (prod.fst : α × β → α) :=
+variables [measurable_space α] [measurable_space β] [measurable_space γ]
+
+lemma measurable_fst : measurable (prod.fst : α × β → α) :=
 measurable.of_comap_le le_sup_left
 
-lemma measurable.fst [measurable_space α] [measurable_space β] [measurable_space γ]
-  {f : α → β × γ} (hf : measurable f) : measurable (λa:α, (f a).1) :=
+lemma measurable.fst {f : α → β × γ} (hf : measurable f) : measurable (λa:α, (f a).1) :=
 measurable_fst.comp hf
 
-lemma measurable_snd [measurable_space α] [measurable_space β] :
-  measurable (prod.snd : α × β → β) :=
+lemma measurable_snd : measurable (prod.snd : α × β → β) :=
 measurable.of_comap_le le_sup_right
 
-lemma measurable.snd [measurable_space α] [measurable_space β] [measurable_space γ]
-  {f : α → β × γ} (hf : measurable f) : measurable (λa:α, (f a).2) :=
+lemma measurable.snd {f : α → β × γ} (hf : measurable f) : measurable (λa:α, (f a).2) :=
 measurable_snd.comp hf
 
-lemma measurable.prod [measurable_space α] [measurable_space β] [measurable_space γ]
-  {f : α → β × γ} (hf₁ : measurable (λa, (f a).1)) (hf₂ : measurable (λa, (f a).2)) :
-  measurable f :=
+lemma measurable.prod {f : α → β × γ}
+  (hf₁ : measurable (λa, (f a).1)) (hf₂ : measurable (λa, (f a).2)) : measurable f :=
 measurable.of_le_map $ sup_le
   (by { rw [measurable_space.comap_le_iff_le_map, measurable_space.map_comp], exact hf₁ })
   (by { rw [measurable_space.comap_le_iff_le_map, measurable_space.map_comp], exact hf₂ })
 
-lemma measurable.prod_mk [measurable_space α] [measurable_space β] [measurable_space γ]
-  {f : α → β} {g : α → γ} (hf : measurable f) (hg : measurable g) : measurable (λa:α, (f a, g a)) :=
+lemma measurable.prod_mk {f : α → β} {g : α → γ} (hf : measurable f) (hg : measurable g) :
+  measurable (λa:α, (f a, g a)) :=
 measurable.prod hf hg
 
-lemma is_measurable.prod [measurable_space α] [measurable_space β] {s : set α} {t : set β}
-  (hs : is_measurable s) (ht : is_measurable t) : is_measurable (set.prod s t) :=
+lemma is_measurable.prod {s : set α} {t : set β} (hs : is_measurable s) (ht : is_measurable t) :
+  is_measurable (s.prod t) :=
 is_measurable.inter (measurable_fst hs) (measurable_snd ht)
 
+lemma is_measurable_prod_of_nonempty {s : set α} {t : set β} (h : (s.prod t).nonempty) :
+  is_measurable (s.prod t) ↔ is_measurable s ∧ is_measurable t :=
+begin
+  rcases h with ⟨⟨x, y⟩, hx, hy⟩,
+  refine ⟨λ hst, _, λ h, h.1.prod h.2⟩,
+  have : is_measurable ((λ x, (x, y)) ⁻¹' s.prod t) := measurable_id.prod_mk measurable_const hst,
+  have : is_measurable (prod.mk x ⁻¹' s.prod t) := measurable_const.prod_mk measurable_id hst,
+  simp * at *
+end
+
+lemma is_measurable_prod {s : set α} {t : set β} :
+  is_measurable (s.prod t) ↔ (is_measurable s ∧ is_measurable t) ∨ s = ∅ ∨ t = ∅ :=
+begin
+  cases (s.prod t).eq_empty_or_nonempty with h h,
+  { simp [h, prod_eq_empty_iff.mp h] },
+  { simp [←not_nonempty_iff_eq_empty, prod_nonempty_iff.mp h, is_measurable_prod_of_nonempty h] }
+end
+
 end prod
 
 section pi

src/topology/metric_space/gromov_hausdorff.lean

@@ -385,7 +385,7 @@ instance GH_space_metric_space : metric_space GH_space :=
            = ((λ (p : nonempty_compacts ℓ_infty_ℝ × nonempty_compacts ℓ_infty_ℝ),
                  Hausdorff_dist ((p.fst).val) ((p.snd).val)) ∘ prod.swap) '' (set.prod {a | ⟦a⟧ = x} {b | ⟦b⟧ = y}) :=
       by { congr, funext, simp, rw Hausdorff_dist_comm },
-    simp only [dist, A, image_comp, prod.swap, image_swap_prod],
+    simp only [dist, A, image_comp, image_swap_prod],
   end,
   eq_of_dist_eq_zero := λx y hxy, begin
     /- To show that two spaces at zero distance are isometric, we argue that the distance

src/topology/subset_properties.lean

@@ -66,7 +66,7 @@ begin
   exact h₂ (h₁ hs)
 end
 
-/-- If `p : set α → Prop` is stable under restriction and union, and each point `x of a compact set `s` 
+/-- If `p : set α → Prop` is stable under restriction and union, and each point `x of a compact set `s`
   has a neighborhood `t` within `s` such that `p t`, then `p s` holds. -/
 @[elab_as_eliminator]
 lemma is_compact.induction_on {s : set α} (hs : is_compact s) {p : set α → Prop} (he : p ∅)
@@ -337,9 +337,9 @@ assume H n hn hp,
   let ⟨u, v, uo, vo, su, tv, p⟩ :=
     H (prod.swap ⁻¹' n)
       (continuous_swap n hn)
-      (by rwa [←image_subset_iff, prod.swap, image_swap_prod]) in
+      (by rwa [←image_subset_iff, image_swap_prod]) in
   ⟨v, u, vo, uo, tv, su,
-    by rwa [←image_subset_iff, prod.swap, image_swap_prod] at p⟩
+    by rwa [←image_subset_iff, image_swap_prod] at p⟩
 
 lemma nhds_contain_boxes.comm {s : set α} {t : set β} :
   nhds_contain_boxes s t ↔ nhds_contain_boxes t s :=