chore(data/set/lattice): Generalize more ⋃/⋂ lemmas to dependent families (#11516)

The "bounded union" and "bounded intersection" are both instances of nested `⋃`/`⋂`. But they only apply when the inner one runs over a predicate `p : ι → Prop`, and the resulting set couldn't depend on `p`. This generalizes to `κ : ι → Sort*` and allows dependence on `κ i`.

The lemmas are renamed from `bUnion`/`bInter` to `Union₂`/`Inter₂` to show that they are more general. Some generalizations lead to unification problems, so I've kept the `b` version around.

Some lemmas were missing between `⋃` and `⋂` or between `⋃`/`⋂` and nested `⋃`/`⋂`, so I'm adding them as well.

Renames

Author: YaelDillies

src/algebra/module/submodule_lattice.lean

@@ -133,7 +133,7 @@ private lemma Inf_le' {S : set (submodule R M)} {p} : p ∈ S → Inf S ≤ p :=
 set.bInter_subset_of_mem
 
 private lemma le_Inf' {S : set (submodule R M)} {p} : (∀q ∈ S, p ≤ q) → p ≤ Inf S :=
-set.subset_bInter
+set.subset_Inter₂
 
 instance : has_inf (submodule R M) :=
 ⟨λ p q,

src/analysis/box_integral/partition/basic.lean

@@ -182,7 +182,7 @@ by simp [← injective_boxes.eq_iff, finset.ext_iff, prepartition.Union, imp_fal
 
 lemma subset_Union (h : J ∈ π) : ↑J ⊆ π.Union := subset_bUnion_of_mem h
 
-lemma Union_subset : π.Union ⊆ I := bUnion_subset π.le_of_mem'
+lemma Union_subset : π.Union ⊆ I := Union₂_subset π.le_of_mem'
 
 @[mono] lemma Union_mono (h : π₁ ≤ π₂) : π₁.Union ⊆ π₂.Union :=
 λ x hx, let ⟨J₁, hJ₁, hx⟩ := π₁.mem_Union.1 hx, ⟨J₂, hJ₂, hle⟩ := h hJ₁
@@ -625,8 +625,8 @@ is_partition_iff_Union_eq.2 $ by simp [h₁.Union_eq, h₂.Union_eq]
 end is_partition
 
 lemma Union_bUnion_partition (h : ∀ J ∈ π, (πi J).is_partition) : (π.bUnion πi).Union = π.Union :=
-(Union_bUnion _ _).trans $ Union_congr id surjective_id $ λ J, Union_congr id surjective_id $ λ hJ,
-  (h J hJ).Union_eq
+(Union_bUnion _ _).trans $ Union_congr_of_surjective id surjective_id $ λ J,
+  Union_congr_of_surjective id surjective_id $ λ hJ, (h J hJ).Union_eq
 
 lemma is_partition_disj_union_of_eq_diff (h : π₂.Union = I \ π₁.Union) :
   is_partition (π₁.disj_union π₂ (h.symm ▸ disjoint_diff)) :=

src/analysis/box_integral/partition/tagged.lean

@@ -62,7 +62,7 @@ lemma Union_def : π.Union = ⋃ J ∈ π, ↑J := rfl
 
 lemma subset_Union (h : J ∈ π) : ↑J ⊆ π.Union := subset_bUnion_of_mem h
 
-lemma Union_subset : π.Union ⊆ I := bUnion_subset π.le_of_mem'
+lemma Union_subset : π.Union ⊆ I := Union₂_subset π.le_of_mem'
 
 /-- A tagged prepartition is a partition if it covers the whole box. -/
 def is_partition := π.to_prepartition.is_partition

src/analysis/convex/simplicial_complex/basic.lean

@@ -139,7 +139,7 @@ begin
 end
 
 lemma vertices_subset_space : K.vertices ⊆ K.space :=
-vertices_eq.subset.trans $ set.bUnion_mono $ λ x hx, subset_convex_hull 𝕜 x
+vertices_eq.subset.trans $ Union₂_mono $ λ x hx, subset_convex_hull 𝕜 x
 
 lemma vertex_mem_convex_hull_iff (hx : x ∈ K.vertices) (hs : s ∈ K.faces) :
   x ∈ convex_hull 𝕜 (s : set E) ↔ x ∈ s :=

src/analysis/normed_space/weak_dual.lean

@@ -170,7 +170,7 @@ variables {E : Type*} [normed_group E] [normed_space 𝕜 E]
 is used, i.e., when `polar 𝕜 s` is interpreted as a subset of `weak_dual 𝕜 E`. -/
 lemma weak_dual.is_closed_polar (s : set E) : is_closed (weak_dual.polar 𝕜 s) :=
 begin
-  rw [weak_dual.polar, polar_eq_Inter, preimage_bInter],
+  rw [weak_dual.polar, polar_eq_Inter, preimage_Inter₂],
   apply is_closed_bInter,
   intros z hz,
   rw set.preimage_set_of_eq,

src/analysis/seminorm.lean

@@ -753,7 +753,7 @@ lemma gauge_lt_one_subset_self (hs : convex ℝ s) (h₀ : (0 : E) ∈ s) (absor
   {x | gauge s x < 1} ⊆ s :=
 begin
   rw gauge_lt_one_eq absorbs,
-  apply set.bUnion_subset,
+  apply set.Union₂_subset,
   rintro r hr _ ⟨y, hy, rfl⟩,
   exact hs.smul_mem_of_zero_mem h₀ hy (Ioo_subset_Icc_self hr),
 end

src/data/set/accumulate.lean

@@ -31,16 +31,16 @@ lemma monotone_accumulate [preorder α] : monotone (accumulate s) :=
 lemma bUnion_accumulate [preorder α] (x : α) : (⋃ y ≤ x, accumulate s y) = ⋃ y ≤ x, s y :=
 begin
   apply subset.antisymm,
-  { exact bUnion_subset (λ x hx, (monotone_accumulate hx : _)) },
-  { exact bUnion_mono (λ x hx, subset_accumulate) }
+  { exact Union₂_subset (λ y hy, monotone_accumulate hy) },
+  { exact Union₂_mono (λ y hy, subset_accumulate) }
 end
 
 lemma Union_accumulate [preorder α] : (⋃ x, accumulate s x) = ⋃ x, s x :=
 begin
   apply subset.antisymm,
   { simp only [subset_def, mem_Union, exists_imp_distrib, mem_accumulate],
     intros z x x' hx'x hz, exact ⟨x', hz⟩ },
-  { exact Union_subset_Union (λ i, subset_accumulate), }
+  { exact Union_mono (λ i, subset_accumulate), }
 end
 
 end set

src/data/set/intervals/disjoint.lean

@@ -92,7 +92,7 @@ variables [linear_order α] {s : set α} {a : α} {f : ι → α}
 
 lemma is_glb.bUnion_Ioi_eq (h : is_glb s a) : (⋃ x ∈ s, Ioi x) = Ioi a :=
 begin
-  refine (bUnion_subset $ λ x hx, _).antisymm (λ x hx, _),
+  refine (Union₂_subset $ λ x hx, _).antisymm (λ x hx, _),
   { exact Ioi_subset_Ioi (h.1 hx) },
   { rcases h.exists_between hx with ⟨y, hys, hay, hyx⟩,
     exact mem_bUnion hys hyx }