Trigger CI for leanprover/lean4#3178

Mathlib/MeasureTheory/Covering/Besicovitch.lean

@@ -1044,10 +1044,10 @@ theorem exists_closedBall_covering_tsum_measure_le (μ : Measure α) [SigmaFinit
 forms a Vitali family. This is essentially a restatement of the measurable Besicovitch theorem. -/
 protected def vitaliFamily (μ : Measure α) [SigmaFinite μ] : VitaliFamily μ where
   setsAt x := (fun r : ℝ => closedBall x r) '' Ioi (0 : ℝ)
-  MeasurableSet' _ := ball_image_iff.2 fun _ _ ↦ isClosed_ball.measurableSet
+  measurableSet _ := ball_image_iff.2 fun _ _ ↦ isClosed_ball.measurableSet
   nonempty_interior _ := ball_image_iff.2 fun r rpos ↦
     (nonempty_ball.2 rpos).mono ball_subset_interior_closedBall
-  Nontrivial x ε εpos := ⟨closedBall x ε, mem_image_of_mem _ εpos, Subset.rfl⟩
+  nontrivial x ε εpos := ⟨closedBall x ε, mem_image_of_mem _ εpos, Subset.rfl⟩
   covering := by
     intro s f fsubset ffine
     let g : α → Set ℝ := fun x => {r | 0 < r ∧ closedBall x r ∈ f x}

Mathlib/MeasureTheory/Covering/Vitali.lean

@@ -404,9 +404,9 @@ protected def vitaliFamily [MetricSpace α] [MeasurableSpace α] [OpensMeasurabl
     VitaliFamily μ where
   setsAt x := { a | IsClosed a ∧ (interior a).Nonempty ∧
     ∃ r, a ⊆ closedBall x r ∧ μ (closedBall x (3 * r)) ≤ C * μ a }
-  MeasurableSet' x a ha := ha.1.measurableSet
+  measurableSet x a ha := ha.1.measurableSet
   nonempty_interior x a ha := ha.2.1
-  Nontrivial x ε εpos := by
+  nontrivial x ε εpos := by
     obtain ⟨r, μr, rpos, rε⟩ :
         ∃ r, μ (closedBall x (3 * r)) ≤ C * μ (closedBall x r) ∧ r ∈ Ioc (0 : ℝ) ε :=
       ((h x).and_eventually (Ioc_mem_nhdsWithin_Ioi ⟨le_rfl, εpos⟩)).exists

Mathlib/MeasureTheory/Covering/VitaliFamily.lean

@@ -66,15 +66,22 @@ differentiations of measure that apply in both contexts.
 -/
 -- @[nolint has_nonempty_instance] -- Porting note: This linter does not exist yet.
 structure VitaliFamily {m : MeasurableSpace α} (μ : Measure α) where
+  /-- Sets of the family "centered" at a given point. -/
   setsAt :  α → Set (Set α)
-  MeasurableSet' : ∀ x : α, ∀ a : Set α, a ∈ setsAt x → MeasurableSet a
-  nonempty_interior : ∀ x : α, ∀ y : Set α, y ∈ setsAt x → (interior y).Nonempty
-  Nontrivial : ∀ (x : α), ∀ ε > (0 : ℝ), ∃ y ∈ setsAt x, y ⊆ closedBall x ε
+  /-- All sets of the family are measurable. -/
+  measurableSet : ∀ x : α, ∀ s ∈ setsAt x, MeasurableSet s
+  /-- All sets of the family have nonempty interior. -/
+  nonempty_interior : ∀ x : α, ∀ s ∈ setsAt x, (interior s).Nonempty
+  /-- For any closed ball around `x`, there exists a set of the family contained in this ball. -/
+  nontrivial : ∀ (x : α), ∀ ε > (0 : ℝ), ∃ s ∈ setsAt x, s ⊆ closedBall x ε
+  /-- Consider a (possibly non-measurable) set `s`,
+  and for any `x` in `s` a subfamily `f x` of `setsAt x`
+  containing sets of arbitrarily small diameter.
+  Then one can extract a disjoint subfamily covering almost all `s`. -/
   covering : ∀ (s : Set α) (f : α → Set (Set α)),
     (∀ x ∈ s, f x ⊆ setsAt x) → (∀ x ∈ s, ∀ ε > (0 : ℝ), ∃ a ∈ f x, a ⊆ closedBall x ε) →
-    ∃ t : Set (α × Set α),
-      (∀ p : α × Set α, p ∈ t → p.1 ∈ s) ∧ (t.PairwiseDisjoint fun p => p.2) ∧
-      (∀ p : α × Set α, p ∈ t → p.2 ∈ f p.1) ∧ μ (s \ ⋃ (p : α × Set α) (_ : p ∈ t), p.2) = 0
+    ∃ t : Set (α × Set α), (∀ p ∈ t, p.1 ∈ s) ∧ (t.PairwiseDisjoint fun p ↦ p.2) ∧
+      (∀ p ∈ t, p.2 ∈ f p.1) ∧ μ (s \ ⋃ p ∈ t, p.2) = 0
 #align vitali_family VitaliFamily
 
 namespace VitaliFamily
@@ -84,13 +91,10 @@ variable {m0 : MeasurableSpace α} {μ : Measure α}
 /-- A Vitali family for a measure `μ` is also a Vitali family for any measure absolutely continuous
 with respect to `μ`. -/
 def mono (v : VitaliFamily μ) (ν : Measure α) (hν : ν ≪ μ) : VitaliFamily ν where
-  setsAt := v.setsAt
-  MeasurableSet' := v.MeasurableSet'
-  nonempty_interior := v.nonempty_interior
-  Nontrivial := v.Nontrivial
-  covering s f h h' := by
-    rcases v.covering s f h h' with ⟨t, ts, disj, mem_f, hμ⟩
-    exact ⟨t, ts, disj, mem_f, hν hμ⟩
+  __ := v
+  covering s f h h' :=
+    let ⟨t, ts, disj, mem_f, hμ⟩ := v.covering s f h h'
+    ⟨t, ts, disj, mem_f, hν hμ⟩
 #align vitali_family.mono VitaliFamily.mono
 
 /-- Given a Vitali family `v` for a measure `μ`, a family `f` is a fine subfamily on a set `s` if
@@ -159,7 +163,7 @@ theorem index_countable [SecondCountableTopology α] : h.index.Countable :=
 
 protected theorem measurableSet_u {p : α × Set α} (hp : p ∈ h.index) :
     MeasurableSet (h.covering p) :=
-  v.MeasurableSet' p.1 _ (h.covering_mem_family hp)
+  v.measurableSet p.1 _ (h.covering_mem_family hp)
 #align vitali_family.fine_subfamily_on.measurable_set_u VitaliFamily.FineSubfamilyOn.measurableSet_u
 
 theorem measure_le_tsum_of_absolutelyContinuous [SecondCountableTopology α] {ρ : Measure α}
@@ -185,15 +189,15 @@ contained in a `δ`-neighborhood on `x`. This does not change the local filter a
 can be convenient to get a nicer global behavior. -/
 def enlarge (v : VitaliFamily μ) (δ : ℝ) (δpos : 0 < δ) : VitaliFamily μ where
   setsAt x := v.setsAt x ∪ { a | MeasurableSet a ∧ (interior a).Nonempty ∧ ¬a ⊆ closedBall x δ }
-  MeasurableSet' x a ha := by
+  measurableSet x a ha := by
     cases' ha with ha ha
-    exacts [v.MeasurableSet' _ _ ha, ha.1]
+    exacts [v.measurableSet _ _ ha, ha.1]
   nonempty_interior x a ha := by
     cases' ha with ha ha
     exacts [v.nonempty_interior _ _ ha, ha.2.1]
-  Nontrivial := by
+  nontrivial := by
     intro x ε εpos
-    rcases v.Nontrivial x ε εpos with ⟨a, ha, h'a⟩
+    rcases v.nontrivial x ε εpos with ⟨a, ha, h'a⟩
     exact ⟨a, mem_union_left _ ha, h'a⟩
   covering := by
     intro s f fset ffine
@@ -237,7 +241,7 @@ instance filterAt_neBot (x : α) : (v.filterAt x).NeBot := by
   simp only [neBot_iff, ← empty_mem_iff_bot, mem_filterAt_iff, not_exists, exists_prop,
     mem_empty_iff_false, and_true_iff, gt_iff_lt, not_and, Ne.def, not_false_iff, not_forall]
   intro ε εpos
-  obtain ⟨w, w_sets, hw⟩ : ∃ w ∈ v.setsAt x, w ⊆ closedBall x ε := v.Nontrivial x ε εpos
+  obtain ⟨w, w_sets, hw⟩ : ∃ w ∈ v.setsAt x, w ⊆ closedBall x ε := v.nontrivial x ε εpos
   exact ⟨w, w_sets, hw⟩
 #align vitali_family.filter_at_ne_bot VitaliFamily.filterAt_neBot
 
@@ -269,7 +273,7 @@ theorem tendsto_filterAt_iff {ι : Type*} {l : Filter ι} {f : ι → Set α} {x
 #align vitali_family.tendsto_filter_at_iff VitaliFamily.tendsto_filterAt_iff
 
 theorem eventually_filterAt_measurableSet (x : α) : ∀ᶠ a in v.filterAt x, MeasurableSet a := by
-  filter_upwards [v.eventually_filterAt_mem_sets x] with _ ha using v.MeasurableSet' _ _ ha
+  filter_upwards [v.eventually_filterAt_mem_sets x] with _ ha using v.measurableSet _ _ ha
 #align vitali_family.eventually_filter_at_measurable_set VitaliFamily.eventually_filterAt_measurableSet
 
 theorem frequently_filterAt_iff {x : α} {P : Set α → Prop} :

Mathlib/Order/Bounds/Basic.lean

@@ -1561,6 +1561,54 @@ end AntitoneMonotone
 
 end Image2
 
+section Prod
+
+variable {α β : Type*} [Preorder α] [Preorder β]
+
+lemma bddAbove_prod {s : Set (α × β)} :
+    BddAbove s ↔ BddAbove (Prod.fst '' s) ∧ BddAbove (Prod.snd '' s) :=
+  ⟨fun ⟨p, hp⟩ ↦ ⟨⟨p.1, ball_image_of_ball fun _q hq ↦ (hp hq).1⟩,
+    ⟨p.2, ball_image_of_ball fun _q hq ↦ (hp hq).2⟩⟩,
+    fun ⟨⟨x, hx⟩, ⟨y, hy⟩⟩ ↦ ⟨⟨x, y⟩, fun _p hp ↦
+      ⟨hx <| mem_image_of_mem _ hp, hy <| mem_image_of_mem _ hp⟩⟩⟩
+
+lemma bddBelow_prod {s : Set (α × β)} :
+    BddBelow s ↔ BddBelow (Prod.fst '' s) ∧ BddBelow (Prod.snd '' s) :=
+  bddAbove_prod (α := αᵒᵈ) (β := βᵒᵈ)
+
+lemma bddAbove_range_prod {F : ι → α × β} :
+    BddAbove (range F) ↔ BddAbove (range <| Prod.fst ∘ F) ∧ BddAbove (range <| Prod.snd ∘ F) := by
+  simp only [bddAbove_prod, ← range_comp]
+
+lemma bddBelow_range_prod {F : ι → α × β} :
+    BddBelow (range F) ↔ BddBelow (range <| Prod.fst ∘ F) ∧ BddBelow (range <| Prod.snd ∘ F) :=
+  bddAbove_range_prod (α := αᵒᵈ) (β := βᵒᵈ)
+
+theorem isLUB_prod [Preorder α] [Preorder β] {s : Set (α × β)} (p : α × β) :
+    IsLUB s p ↔ IsLUB (Prod.fst '' s) p.1 ∧ IsLUB (Prod.snd '' s) p.2 := by
+  refine'
+    ⟨fun H =>
+      ⟨⟨monotone_fst.mem_upperBounds_image H.1, fun a ha => _⟩,
+        ⟨monotone_snd.mem_upperBounds_image H.1, fun a ha => _⟩⟩,
+      fun H => ⟨_, _⟩⟩
+  · suffices h : (a, p.2) ∈ upperBounds s from (H.2 h).1
+    exact fun q hq => ⟨ha <| mem_image_of_mem _ hq, (H.1 hq).2⟩
+  · suffices h : (p.1, a) ∈ upperBounds s from (H.2 h).2
+    exact fun q hq => ⟨(H.1 hq).1, ha <| mem_image_of_mem _ hq⟩
+  · exact fun q hq => ⟨H.1.1 <| mem_image_of_mem _ hq, H.2.1 <| mem_image_of_mem _ hq⟩
+  · exact fun q hq =>
+      ⟨H.1.2 <| monotone_fst.mem_upperBounds_image hq,
+        H.2.2 <| monotone_snd.mem_upperBounds_image hq⟩
+#align is_lub_prod isLUB_prod
+
+theorem isGLB_prod [Preorder α] [Preorder β] {s : Set (α × β)} (p : α × β) :
+    IsGLB s p ↔ IsGLB (Prod.fst '' s) p.1 ∧ IsGLB (Prod.snd '' s) p.2 :=
+  @isLUB_prod αᵒᵈ βᵒᵈ _ _ _ _
+#align is_glb_prod isGLB_prod
+
+end Prod
+
+
 section Pi
 
 variable {π : α → Type*} [∀ a, Preorder (π a)]
@@ -1614,28 +1662,6 @@ theorem IsLUB.of_image [Preorder α] [Preorder β] {f : α → β} (hf : ∀ {x
     hf.1 <| hx.2 <| Monotone.mem_upperBounds_image (fun _ _ => hf.2) hy⟩
 #align is_lub.of_image IsLUB.of_image
 
-theorem isLUB_prod [Preorder α] [Preorder β] {s : Set (α × β)} (p : α × β) :
-    IsLUB s p ↔ IsLUB (Prod.fst '' s) p.1 ∧ IsLUB (Prod.snd '' s) p.2 := by
-  refine'
-    ⟨fun H =>
-      ⟨⟨monotone_fst.mem_upperBounds_image H.1, fun a ha => _⟩,
-        ⟨monotone_snd.mem_upperBounds_image H.1, fun a ha => _⟩⟩,
-      fun H => ⟨_, _⟩⟩
-  · suffices h : (a, p.2) ∈ upperBounds s from (H.2 h).1
-    exact fun q hq => ⟨ha <| mem_image_of_mem _ hq, (H.1 hq).2⟩
-  · suffices h : (p.1, a) ∈ upperBounds s from (H.2 h).2
-    exact fun q hq => ⟨(H.1 hq).1, ha <| mem_image_of_mem _ hq⟩
-  · exact fun q hq => ⟨H.1.1 <| mem_image_of_mem _ hq, H.2.1 <| mem_image_of_mem _ hq⟩
-  · exact fun q hq =>
-      ⟨H.1.2 <| monotone_fst.mem_upperBounds_image hq,
-        H.2.2 <| monotone_snd.mem_upperBounds_image hq⟩
-#align is_lub_prod isLUB_prod
-
-theorem isGLB_prod [Preorder α] [Preorder β] {s : Set (α × β)} (p : α × β) :
-    IsGLB s p ↔ IsGLB (Prod.fst '' s) p.1 ∧ IsGLB (Prod.snd '' s) p.2 :=
-  @isLUB_prod αᵒᵈ βᵒᵈ _ _ _ _
-#align is_glb_prod isGLB_prod
-
 section ScottContinuous
 variable [Preorder α] [Preorder β] {f : α → β} {a : α}