feat(data/set/*): lemmas about monotone/antitone and sets/interva…

…ls (#11173)

* Rename `set.monotone_inter` and `set.monotone_union` to
  `monotone.inter` and `monotone.union`.
* Add `antitone` versions of some `monotone` lemmas.
* Specialize `Union_Inter_of_monotone` for `set.pi`.
* Add lemmas about `⋃ x, Ioi (f x)`, `⋃ x, Iio (f x)`, and `⋃ x, Ioo (f x) (g x)`.
* Add dot notation lemmas `monotone.Ixx` and `antitone.Ixx`.

src/data/set/finite.lean

@@ -638,6 +638,20 @@ begin
   exact or.inr ⟨i, finset.mem_univ i, le_rfl⟩
 end
 
+lemma Union_pi_of_monotone {ι ι' : Type*} [linear_order ι'] [nonempty ι'] {α : ι → Type*}
+  {I : set ι} {s : Π i, ι' → set (α i)} (hI : finite I) (hs : ∀ i ∈ I, monotone (s i)) :
+  (⋃ j : ι', I.pi (λ i, s i j)) = I.pi (λ i, ⋃ j, s i j) :=
+begin
+  simp only [pi_def, bInter_eq_Inter, preimage_Union],
+  haveI := hI.fintype,
+  exact Union_Inter_of_monotone (λ i j₁ j₂ h, preimage_mono $ hs i i.2 h)
+end
+
+lemma Union_univ_pi_of_monotone {ι ι' : Type*} [linear_order ι'] [nonempty ι'] [fintype ι]
+  {α : ι → Type*} {s : Π i, ι' → set (α i)} (hs : ∀ i, monotone (s i)) :
+  (⋃ j : ι', pi univ (λ i, s i j)) = pi univ (λ i, ⋃ j, s i j) :=
+Union_pi_of_monotone (finite.of_fintype _) (λ i _, hs i)
+
 instance nat.fintype_Iio (n : ℕ) : fintype (Iio n) :=
 fintype.of_finset (finset.range n) $ by simp
 

src/data/set/intervals/disjoint.lean

@@ -13,11 +13,11 @@ because this would create an `import` cycle. Namely, lemmas in this file can use
 from `data.set.lattice`, including `disjoint`.
 -/
 
-universe u
+universes u v w
 
-variables {α : Type u}
+variables {ι : Sort u} {α : Type v} {β : Type w}
 
-open order_dual (to_dual)
+open set order_dual (to_dual)
 
 namespace set
 
@@ -66,22 +66,48 @@ begin
   exact h.elim (λ h, absurd hx (not_lt_of_le h)) id
 end
 
-@[simp] lemma Union_Ico_eq_Iio_self_iff {ι : Sort*} {f : ι → α} {a : α} :
+@[simp] lemma Union_Ico_eq_Iio_self_iff {f : ι → α} {a : α} :
   (⋃ i, Ico (f i) a) = Iio a ↔ ∀ x < a, ∃ i, f i ≤ x :=
 by simp [← Ici_inter_Iio, ← Union_inter, subset_def]
 
-@[simp] lemma Union_Ioc_eq_Ioi_self_iff {ι : Sort*} {f : ι → α} {a : α} :
+@[simp] lemma Union_Ioc_eq_Ioi_self_iff {f : ι → α} {a : α} :
   (⋃ i, Ioc a (f i)) = Ioi a ↔ ∀ x, a < x → ∃ i, x ≤ f i :=
 by simp [← Ioi_inter_Iic, ← inter_Union, subset_def]
 
-@[simp] lemma bUnion_Ico_eq_Iio_self_iff {ι : Sort*} {p : ι → Prop} {f : Π i, p i → α} {a : α} :
+@[simp] lemma bUnion_Ico_eq_Iio_self_iff {p : ι → Prop} {f : Π i, p i → α} {a : α} :
   (⋃ i (hi : p i), Ico (f i hi) a) = Iio a ↔ ∀ x < a, ∃ i hi, f i hi ≤ x :=
 by simp [← Ici_inter_Iio, ← Union_inter, subset_def]
 
-@[simp] lemma bUnion_Ioc_eq_Ioi_self_iff {ι : Sort*} {p : ι → Prop} {f : Π i, p i → α} {a : α} :
+@[simp] lemma bUnion_Ioc_eq_Ioi_self_iff {p : ι → Prop} {f : Π i, p i → α} {a : α} :
   (⋃ i (hi : p i), Ioc a (f i hi)) = Ioi a ↔ ∀ x, a < x → ∃ i hi, x ≤ f i hi :=
 by simp [← Ioi_inter_Iic, ← inter_Union, subset_def]
 
 end linear_order
 
 end set
+
+section Union_Ixx
+
+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, _),
+  { exact Ioi_subset_Ioi (h.1 hx) },
+  { rcases h.exists_between hx with ⟨y, hys, hay, hyx⟩,
+    exact mem_bUnion hys hyx }
+end
+
+lemma is_glb.Union_Ioi_eq (h : is_glb (range f) a) :
+  (⋃ x, Ioi (f x)) = Ioi a :=
+bUnion_range.symm.trans h.bUnion_Ioi_eq
+
+lemma is_lub.bUnion_Iio_eq (h : is_lub s a) :
+  (⋃ x ∈ s, Iio x) = Iio a :=
+h.dual.bUnion_Ioi_eq
+
+lemma is_lub.Union_Iio_eq (h : is_lub (range f) a) :
+  (⋃ x, Iio (f x)) = Iio a :=
+h.dual.Union_Ioi_eq
+
+end Union_Ixx

src/data/set/intervals/monotone.lean

@@ -3,7 +3,7 @@ Copyright (c) 2021 Yury Kudryashov. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov
 -/
-import data.set.intervals.basic
+import data.set.intervals.disjoint
 import tactic.field_simp
 
 /-!
@@ -51,6 +51,8 @@ protected lemma antitone_on.Iic_union_Ici (h₁ : antitone_on f (Iic a))
 
 end
 
+section ordered_group
+
 variables {G H : Type*} [linear_ordered_add_comm_group G] [ordered_add_comm_group H]
 
 lemma strict_mono_of_odd_strict_mono_on_nonneg {f : G → H} (h₁ : ∀ x, f (-x) = -f x)
@@ -70,11 +72,13 @@ begin
   exact h₂ (neg_nonneg.2 hy) (neg_nonneg.2 hx) (neg_le_neg hxy)
 end
 
-variables (k : Type*) [linear_ordered_field k]
+end ordered_group
 
 /-- In a linear ordered field, the whole field is order isomorphic to the open interval `(-1, 1)`.
+We consider the actual implementation to be a "black box", so it is irreducible.
 -/
-@[irreducible] def order_iso_Ioo_neg_one_one : k ≃o Ioo (-1 : k) 1 :=
+@[irreducible] def order_iso_Ioo_neg_one_one (k : Type*) [linear_ordered_field k] :
+  k ≃o Ioo (-1 : k) 1 :=
 begin
   refine strict_mono.order_iso_of_right_inverse _ _ (λ x, x / (1 - |x|)) _,
   { refine cod_restrict (λ x, x / (1 + |x|)) _ (λ x, abs_lt.1 _),
@@ -90,3 +94,86 @@ begin
     have : 0 < 1 - |(x : k)|, from sub_pos.2 (abs_lt.2 x.2),
     field_simp [abs_div, this.ne', abs_of_pos this] }
 end
+
+section Ixx
+
+variables {α β : Type*} [preorder α] [preorder β] {f g : α → β}
+
+lemma antitone_Ici : antitone (Ici : α → set α) := λ _ _, Ici_subset_Ici.2
+
+lemma monotone_Iic : monotone (Iic : α → set α) := λ _ _, Iic_subset_Iic.2
+
+lemma antitone_Ioi : antitone (Ioi : α → set α) := λ _ _, Ioi_subset_Ioi
+
+lemma monotone_Iio : monotone (Iio : α → set α) := λ _ _, Iio_subset_Iio
+
+protected lemma monotone.Ici (hf : monotone f) : antitone (λ x, Ici (f x)) :=
+antitone_Ici.comp_monotone hf
+
+protected lemma antitone.Ici (hf : antitone f) : monotone (λ x, Ici (f x)) :=
+antitone_Ici.comp hf
+
+protected lemma monotone.Iic (hf : monotone f) : monotone (λ x, Iic (f x)) :=
+monotone_Iic.comp hf
+
+protected lemma antitone.Iic (hf : antitone f) : antitone (λ x, Iic (f x)) :=
+monotone_Iic.comp_antitone hf
+
+protected lemma monotone.Ioi (hf : monotone f) : antitone (λ x, Ioi (f x)) :=
+antitone_Ioi.comp_monotone hf
+
+protected lemma antitone.Ioi (hf : antitone f) : monotone (λ x, Ioi (f x)) :=
+antitone_Ioi.comp hf
+
+protected lemma monotone.Iio (hf : monotone f) : monotone (λ x, Iio (f x)) :=
+monotone_Iio.comp hf
+
+protected lemma antitone.Iio (hf : antitone f) : antitone (λ x, Iio (f x)) :=
+monotone_Iio.comp_antitone hf
+
+protected lemma monotone.Icc (hf : monotone f) (hg : antitone g) :
+  antitone (λ x, Icc (f x) (g x)) :=
+hf.Ici.inter hg.Iic
+
+protected lemma antitone.Icc (hf : antitone f) (hg : monotone g) :
+  monotone (λ x, Icc (f x) (g x)) :=
+hf.Ici.inter hg.Iic
+
+protected lemma monotone.Ico (hf : monotone f) (hg : antitone g) :
+  antitone (λ x, Ico (f x) (g x)) :=
+hf.Ici.inter hg.Iio
+
+protected lemma antitone.Ico (hf : antitone f) (hg : monotone g) :
+  monotone (λ x, Ico (f x) (g x)) :=
+hf.Ici.inter hg.Iio
+
+protected lemma monotone.Ioc (hf : monotone f) (hg : antitone g) :
+  antitone (λ x, Ioc (f x) (g x)) :=
+hf.Ioi.inter hg.Iic
+
+protected lemma antitone.Ioc (hf : antitone f) (hg : monotone g) :
+  monotone (λ x, Ioc (f x) (g x)) :=
+hf.Ioi.inter hg.Iic
+
+protected lemma monotone.Ioo (hf : monotone f) (hg : antitone g) :
+  antitone (λ x, Ioo (f x) (g x)) :=
+hf.Ioi.inter hg.Iio
+
+protected lemma antitone.Ioo (hf : antitone f) (hg : monotone g) :
+  monotone (λ x, Ioo (f x) (g x)) :=
+hf.Ioi.inter hg.Iio
+
+end Ixx
+
+section Union
+
+variables {α β : Type*} [semilattice_sup α] [linear_order β] {f g : α → β} {a b : β}
+
+lemma Union_Ioo_of_mono_of_is_glb_of_is_lub (hf : antitone f) (hg : monotone g)
+  (ha : is_glb (range f) a) (hb : is_lub (range g) b) :
+  (⋃ x, Ioo (f x) (g x)) = Ioo a b :=
+calc (⋃ x, Ioo (f x) (g x)) = (⋃ x, Ioi (f x)) ∩ ⋃ x, Iio (g x) :
+  Union_inter_of_monotone hf.Ioi hg.Iio
+... = Ioi a ∩ Iio b : congr_arg2 (∩) ha.Union_Ioi_eq hb.Union_Iio_eq
+
+end Union

src/data/set/lattice.lean

@@ -99,18 +99,30 @@ instance : complete_boolean_algebra (set α) :=
 lemma monotone_image {f : α → β} : monotone (image f) :=
 λ s t, image_subset _
 
-theorem monotone_inter [preorder β] {f g : β → set α}
+theorem _root_.monotone.inter [preorder β] {f g : β → set α}
   (hf : monotone f) (hg : monotone g) : monotone (λ x, f x ∩ g x) :=
-λ b₁ b₂ h, inter_subset_inter (hf h) (hg h)
+hf.inf hg
 
-theorem monotone_union [preorder β] {f g : β → set α}
+theorem _root_.antitone.inter [preorder β] {f g : β → set α}
+  (hf : antitone f) (hg : antitone g) : antitone (λ x, f x ∩ g x) :=
+hf.inf hg
+
+theorem _root_.monotone.union [preorder β] {f g : β → set α}
   (hf : monotone f) (hg : monotone g) : monotone (λ x, f x ∪ g x) :=
-λ b₁ b₂ h, union_subset_union (hf h) (hg h)
+hf.sup hg
+
+theorem _root_.antitone.union [preorder β] {f g : β → set α}
+  (hf : antitone f) (hg : antitone g) : antitone (λ x, f x ∪ g x) :=
+hf.sup hg
 
 theorem monotone_set_of [preorder α] {p : α → β → Prop}
   (hp : ∀ b, monotone (λ a, p a b)) : monotone (λ a, {b | p a b}) :=
 λ a a' h b, hp b h
 
+theorem antitone_set_of [preorder α] {p : α → β → Prop}
+  (hp : ∀ b, antitone (λ a, p a b)) : antitone (λ a, {b | p a b}) :=
+λ a a' h b, hp b h
+
 section galois_connection
 variables {f : α → β}
 

src/order/lattice.lean

@@ -759,6 +759,50 @@ lemma map_inf [semilattice_inf α] [is_total α (≤)] [semilattice_inf β] {f :
 
 end monotone
 
+namespace antitone
+
+/-- Pointwise supremum of two monotone functions is a monotone function. -/
+protected lemma sup [preorder α] [semilattice_sup β] {f g : α → β} (hf : antitone f)
+  (hg : antitone g) : antitone (f ⊔ g) :=
+λ x y h, sup_le_sup (hf h) (hg h)
+
+/-- Pointwise infimum of two monotone functions is a monotone function. -/
+protected lemma inf [preorder α] [semilattice_inf β] {f g : α → β} (hf : antitone f)
+  (hg : antitone g) : antitone (f ⊓ g) :=
+λ x y h, inf_le_inf (hf h) (hg h)
+
+/-- Pointwise maximum of two monotone functions is a monotone function. -/
+protected lemma max [preorder α] [linear_order β] {f g : α → β} (hf : antitone f)
+  (hg : antitone g) : antitone (λ x, max (f x) (g x)) :=
+hf.sup hg
+
+/-- Pointwise minimum of two monotone functions is a monotone function. -/
+protected lemma min [preorder α] [linear_order β] {f g : α → β} (hf : antitone f)
+  (hg : antitone g) : antitone (λ x, min (f x) (g x)) :=
+hf.inf hg
+
+lemma map_sup_le [semilattice_sup α] [semilattice_inf β]
+  {f : α → β} (h : antitone f) (x y : α) :
+  f (x ⊔ y) ≤ f x ⊓ f y :=
+h.dual_right.le_map_sup x y
+
+lemma map_sup [semilattice_sup α] [is_total α (≤)] [semilattice_inf β] {f : α → β}
+  (hf : antitone f) (x y : α) :
+  f (x ⊔ y) = f x ⊓ f y :=
+hf.dual_right.map_sup x y
+
+lemma le_map_inf [semilattice_inf α] [semilattice_sup β]
+  {f : α → β} (h : antitone f) (x y : α) :
+  f x ⊔ f y ≤ f (x ⊓ y) :=
+h.dual_right.map_inf_le x y
+
+lemma map_inf [semilattice_inf α] [is_total α (≤)] [semilattice_sup β] {f : α → β}
+  (hf : antitone f) (x y : α) :
+  f (x ⊓ y) = f x ⊔ f y :=
+hf.dual_right.map_inf x y
+
+end antitone
+
 /-!
 ### Products of (semi-)lattices
 -/

src/topology/uniform_space/basic.lean

@@ -771,7 +771,7 @@ calc (a, b) ∈ closure t ↔ (𝓝 (a, b) ⊓ 𝓟 t ≠ ⊥) : mem_closure_iff
   ... ↔ (∀s ∈ 𝓤 α, (set.prod {y : α | (a, y) ∈ s} {x : α | (x, b) ∈ s} ∩ t).nonempty) :
   begin
     rw [lift'_inf_principal_eq, ← ne_bot_iff, lift'_ne_bot_iff],
-    exact monotone_inter (monotone_prod monotone_preimage monotone_preimage) monotone_const
+    exact (monotone_prod monotone_preimage monotone_preimage).inter monotone_const
   end
   ... ↔ (∀ s ∈ 𝓤 α, (a, b) ∈ s ○ (t ○ s)) :
     forall_congr $ assume s, forall_congr $ assume hs,

src/topology/uniform_space/completion.lean

@@ -175,7 +175,7 @@ have h_ex : ∀ s ∈ 𝓤 (Cauchy α), ∃y:α, (f, pure_cauchy y) ∈ s, from
 begin
   simp only [closure_eq_cluster_pts, cluster_pt, nhds_eq_uniformity, lift'_inf_principal_eq,
     set.inter_comm _ (range pure_cauchy), mem_set_of_eq],
-  exact (lift'_ne_bot_iff $ monotone_inter monotone_const monotone_preimage).mpr
+  exact (lift'_ne_bot_iff $ monotone_const.inter monotone_preimage).mpr
     (assume s hs,
       let ⟨y, hy⟩ := h_ex s hs in
       have pure_cauchy y ∈ range pure_cauchy ∩ {y : Cauchy α | (f, y) ∈ s},

src/topology/uniform_space/uniform_embedding.lean

@@ -200,7 +200,7 @@ begin
   intros b' hb',
   rw [nhds_eq_uniformity, lift'_inf_principal_eq, lift'_ne_bot_iff],
   exact assume s, this b' s hb',
-  exact monotone_inter monotone_preimage monotone_const
+  exact monotone_preimage.inter monotone_const
 end,
 have ∀b', (b, b') ∈ t → b' ∈ closure (e '' {a' | (a, a') ∈ s}),
   from assume b' hb', by rw [closure_eq_cluster_pts]; exact this b' hb',