chore(measure_theory/measurable_space): add `finset.is_measurable_bUn…

…ion` etc (#4553)

I always forget how to convert `finset` or `set.finite` to `set.countable. Also `finset.is_measurable_bUnion` uses `finset`'s `has_mem`, not coercion to `set`.

Also replace `tendsto_at_top_supr_nat` etc with slightly more general versions using a `[semilattice_sup β] [nonempty β]` instead of `nat`.

src/measure_theory/borel_space.lean

@@ -174,7 +174,7 @@ opens_measurable_space.borel_le _ $ generate_measurable.basic _ h
 lemma is_measurable_interior : is_measurable (interior s) := is_open_interior.is_measurable
 
 lemma is_closed.is_measurable (h : is_closed s) : is_measurable s :=
-is_measurable.compl_iff.1 $ h.is_measurable
+h.is_measurable.of_compl
 
 lemma is_compact.is_measurable [t2_space α] (h : is_compact s) : is_measurable s :=
 h.is_closed.is_measurable

src/measure_theory/measurable_space.lean

@@ -125,10 +125,25 @@ begin
   exact is_measurable.Union (by simpa using h)
 end
 
+lemma set.finite.is_measurable_bUnion {f : β → set α} {s : set β} (hs : finite s)
+  (h : ∀ b ∈ s, is_measurable (f b)) :
+  is_measurable (⋃ b ∈ s, f b) :=
+is_measurable.bUnion hs.countable h
+
+lemma finset.is_measurable_bUnion {f : β → set α} (s : finset β)
+  (h : ∀ b ∈ s, is_measurable (f b)) :
+  is_measurable (⋃ b ∈ s, f b) :=
+s.finite_to_set.is_measurable_bUnion h
+
 lemma is_measurable.sUnion {s : set (set α)} (hs : countable s) (h : ∀t∈s, is_measurable t) :
   is_measurable (⋃₀ s) :=
 by { rw sUnion_eq_bUnion, exact is_measurable.bUnion hs h }
 
+lemma set.finite.is_measurable_sUnion {s : set (set α)} (hs : finite s)
+  (h : ∀ t ∈ s, is_measurable t) :
+  is_measurable (⋃₀ s) :=
+is_measurable.sUnion hs.countable h
+
 lemma is_measurable.Union_Prop {p : Prop} {f : p → set α} (hf : ∀b, is_measurable (f b)) :
   is_measurable (⋃b, f b) :=
 by { by_cases p; simp [h, hf, is_measurable.empty] }
@@ -143,10 +158,22 @@ lemma is_measurable.bInter {f : β → set α} {s : set β} (hs : countable s)
 is_measurable.compl_iff.1 $
 by { rw compl_bInter, exact is_measurable.bUnion hs (λ b hb, (h b hb).compl) }
 
+lemma set.finite.is_measurable_bInter {f : β → set α} {s : set β} (hs : finite s)
+  (h : ∀b∈s, is_measurable (f b)) : is_measurable (⋂b∈s, f b) :=
+is_measurable.bInter hs.countable h
+
+lemma finset.is_measurable_bInter {f : β → set α} (s : finset β)
+  (h : ∀b∈s, is_measurable (f b)) : is_measurable (⋂b∈s, f b) :=
+s.finite_to_set.is_measurable_bInter h
+
 lemma is_measurable.sInter {s : set (set α)} (hs : countable s) (h : ∀t∈s, is_measurable t) :
   is_measurable (⋂₀ s) :=
 by { rw sInter_eq_bInter, exact is_measurable.bInter hs h }
 
+lemma set.finite.is_measurable_sInter {s : set (set α)} (hs : finite s)
+  (h : ∀t∈s, is_measurable t) : is_measurable (⋂₀ s) :=
+is_measurable.sInter hs.countable h
+
 lemma is_measurable.Inter_Prop {p : Prop} {f : p → set α} (hf : ∀b, is_measurable (f b)) :
   is_measurable (⋂b, f b) :=
 by { by_cases p; simp [h, hf, is_measurable.univ] }
@@ -472,7 +499,7 @@ end
 
 @[simp] lemma measurable_const {α β} [measurable_space α] [measurable_space β] {a : α} :
   measurable (λb:β, a) :=
-by { intros s hs, by_cases a ∈ s; simp [*, preimage] }
+assume s hs, is_measurable.const (a ∈ s)
 
 lemma measurable.indicator [measurable_space α] [measurable_space β] [has_zero β]
   {s : set α} {f : α → β} (hf : measurable f) (hs : is_measurable s) :
@@ -507,8 +534,7 @@ begin
 end
 
 lemma measurable_unit [measurable_space α] (f : unit → α) : measurable f :=
-have f = (λu, f ()) := funext $ assume ⟨⟩, rfl,
-by { rw this, exact measurable_const }
+measurable_from_top
 
 section nat
 

src/measure_theory/measure_space.lean

@@ -274,10 +274,8 @@ lemma measure_bUnion {s : set β} {f : β → set α} (hs : countable s)
   μ (⋃b∈s, f b) = ∑'p:s, μ (f p) :=
 begin
   haveI := hs.to_encodable,
-  rw [← measure_Union, bUnion_eq_Union],
-  { rintro ⟨i, hi⟩ ⟨j, hj⟩ ij x ⟨h₁, h₂⟩,
-    exact hd i hi j hj (mt subtype.ext_val ij:_) ⟨h₁, h₂⟩ },
-  { simpa }
+  rw bUnion_eq_Union,
+  exact measure_Union (hd.on_injective subtype.coe_injective $ λ x, x.2) (λ x, h x x.2)
 end
 
 lemma measure_sUnion {S : set (set α)} (hs : countable S)
@@ -431,7 +429,7 @@ lemma tendsto_measure_Union {μ : measure α} {s : ℕ → set α}
   tendsto (μ ∘ s) at_top (𝓝 (μ (⋃ n, s n))) :=
 begin
   rw measure_Union_eq_supr hs (directed_of_sup hm),
-  exact tendsto_at_top_supr_nat (μ ∘ s) (assume n m hnm, measure_mono $ hm hnm)
+  exact tendsto_at_top_supr (assume n m hnm, measure_mono $ hm hnm)
 end
 
 /-- Continuity from above: the measure of the intersection of a decreasing sequence of measurable
@@ -441,7 +439,7 @@ lemma tendsto_measure_Inter {μ : measure α} {s : ℕ → set α}
   tendsto (μ ∘ s) at_top (𝓝 (μ (⋂ n, s n))) :=
 begin
   rw measure_Inter_eq_infi hs (directed_of_sup hm) hf,
-  exact tendsto_at_top_infi_nat (μ ∘ s) (assume n m hnm, measure_mono $ hm hnm),
+  exact tendsto_at_top_infi (assume n m hnm, measure_mono $ hm hnm),
 end
 
 /-- One direction of the Borel-Cantelli lemma: if (sᵢ) is a sequence of measurable sets such that
@@ -918,7 +916,7 @@ begin
   induction s using finset.induction_on with i s hi hs, { simp },
   simp only [finset.mem_insert, or_imp_distrib, forall_and_distrib, forall_eq] at htm ⊢,
   simp only [finset.bUnion_insert, ← hs htm.2],
-  exact restrict_union_congr htm.1 (is_measurable.bUnion s.countable_to_set htm.2)
+  exact restrict_union_congr htm.1 (s.is_measurable_bUnion htm.2)
 end
 
 lemma restrict_Union_congr [encodable ι] {s : ι → set α} (hm : ∀ i, is_measurable (s i)) :
@@ -928,7 +926,7 @@ begin
   refine ⟨λ h i, restrict_congr_mono (subset_Union _ _) (hm i) h, λ h, _⟩,
   ext1 t ht,
   have M : ∀ t : finset ι, is_measurable (⋃ i ∈ t, s i) :=
-    λ t, is_measurable.bUnion t.countable_to_set (λ i _, hm i),
+    λ t, t.is_measurable_bUnion (λ i _, hm i),
   have D : directed (⊆) (λ t : finset ι, ⋃ i ∈ t, s i) :=
     directed_of_sup (λ t₁ t₂ ht, bUnion_subset_bUnion_left ht),
   rw [Union_eq_Union_finset],

src/topology/algebra/ordered.lean

@@ -2464,25 +2464,6 @@ begin
         infi_le_of_le (a + r) $ infi_le _ (or.inr rfl)) } }
 end
 
-lemma tendsto_at_top_supr_nat [topological_space α] [complete_linear_order α] [order_topology α]
-  (f : ℕ → α) (hf : monotone f) : tendsto f at_top (𝓝 (⨆i, f i)) :=
-tendsto_order.2 $ and.intro
-  (assume a ha, let ⟨n, hn⟩ := lt_supr_iff.1 ha in
-    mem_at_top_sets.2 ⟨n, assume i hi, lt_of_lt_of_le hn (hf hi)⟩)
-  (assume a ha, univ_mem_sets' (assume n, lt_of_le_of_lt (le_supr _ n) ha))
-
-lemma tendsto_at_top_infi_nat [topological_space α] [complete_linear_order α] [order_topology α]
-  (f : ℕ → α) (hf : ∀{n m}, n ≤ m → f m ≤ f n) : tendsto f at_top (𝓝 (⨅i, f i)) :=
-@tendsto_at_top_supr_nat (order_dual α) _ _ _ _ @hf
-
-lemma supr_eq_of_tendsto {α} [topological_space α] [complete_linear_order α] [order_topology α]
-  {f : ℕ → α} {a : α} (hf : monotone f) : tendsto f at_top (𝓝 a) → supr f = a :=
-tendsto_nhds_unique (tendsto_at_top_supr_nat f hf)
-
-lemma infi_eq_of_tendsto {α} [topological_space α] [complete_linear_order α] [order_topology α]
-  {f : ℕ → α} {a : α} (hf : ∀n m, n ≤ m → f m ≤ f n) : tendsto f at_top (𝓝 a) → infi f = a :=
-tendsto_nhds_unique (tendsto_at_top_infi_nat f hf)
-
 /-- $\lim_{x\to+\infty}|x|=+\infty$ -/
 lemma tendsto_abs_at_top_at_top [decidable_linear_ordered_add_comm_group α] :
   tendsto (abs : α → α) at_top at_top :=
@@ -2549,17 +2530,38 @@ begin
   { exact tendsto_of_not_nonempty hi }
 end
 
+lemma tendsto_at_top_cinfi {ι α : Type*} [preorder ι] [topological_space α]
+  [conditionally_complete_linear_order α] [order_topology α]
+  {f : ι → α} (h_mono : ∀ ⦃i j⦄, i ≤ j → f j ≤ f i) (hbdd : bdd_below $ range f) :
+  tendsto f at_top (𝓝 (⨅i, f i)) :=
+@tendsto_at_top_csupr _ (order_dual α) _ _ _ _ _ @h_mono hbdd
+
 lemma tendsto_at_top_supr {ι α : Type*} [preorder ι] [topological_space α]
   [complete_linear_order α] [order_topology α] {f : ι → α} (h_mono : monotone f) :
   tendsto f at_top (𝓝 (⨆i, f i)) :=
 tendsto_at_top_csupr h_mono (order_top.bdd_above _)
 
+lemma tendsto_at_top_infi {ι α : Type*} [preorder ι] [topological_space α]
+  [complete_linear_order α] [order_topology α] {f : ι → α} (h_mono : ∀ ⦃i j⦄, i ≤ j → f j ≤ f i) :
+  tendsto f at_top (𝓝 (⨅i, f i)) :=
+tendsto_at_top_cinfi @h_mono (order_bot.bdd_below _)
+
 lemma tendsto_of_monotone {ι α : Type*} [preorder ι] [topological_space α]
   [conditionally_complete_linear_order α] [order_topology α] {f : ι → α} (h_mono : monotone f) :
   tendsto f at_top at_top ∨ (∃ l, tendsto f at_top (𝓝 l)) :=
 if H : bdd_above (range f) then or.inr ⟨_, tendsto_at_top_csupr h_mono H⟩
 else or.inl $ tendsto_at_top_at_top_of_monotone' h_mono H
 
+lemma supr_eq_of_tendsto {α β} [topological_space α] [complete_linear_order α] [order_topology α]
+  [nonempty β] [semilattice_sup β] {f : β → α} {a : α} (hf : monotone f) :
+  tendsto f at_top (𝓝 a) → supr f = a :=
+tendsto_nhds_unique (tendsto_at_top_supr hf)
+
+lemma infi_eq_of_tendsto {α} [topological_space α] [complete_linear_order α] [order_topology α]
+  [nonempty β] [semilattice_sup β] {f : β → α} {a : α} (hf : ∀n m, n ≤ m → f m ≤ f n) :
+  tendsto f at_top (𝓝 a) → infi f = a :=
+tendsto_nhds_unique (tendsto_at_top_infi hf)
+
 @[to_additive] lemma tendsto_inv_nhds_within_Ioi [ordered_comm_group α]
   [topological_space α] [topological_group α] {a : α} :
   tendsto has_inv.inv (𝓝[Ioi a] a) (𝓝[Iio (a⁻¹)] (a⁻¹)) :=