chore(data/set/*,order/*): add missing lemmas about monotone_on etc (…

…#14943)

* Add `monotone_on`/`antitone`/`antitone_on` versions of existing `monotone` lemmas for `id`/`const`, `inf`/`sup`/`min`/`max`, `inter`/`union`, and intervals.
* Drop `set.monotone_prod`, leave `monotone.set_prod` only.
* Golf some proofs that were broken by removal of `set.monotone_prod`.

src/data/set/intervals/monotone.lean

@@ -97,7 +97,7 @@ end
 
 section Ixx
 
-variables {α β : Type*} [preorder α] [preorder β] {f g : α → β}
+variables {α β : Type*} [preorder α] [preorder β] {f g : α → β} {s : set α}
 
 lemma antitone_Ici : antitone (Ici : α → set α) := λ _ _, Ici_subset_Ici.2
 
@@ -110,59 +110,115 @@ 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 monotone_on.Ici (hf : monotone_on f s) : antitone_on (λ x, Ici (f x)) s :=
+antitone_Ici.comp_monotone_on hf
+
 protected lemma antitone.Ici (hf : antitone f) : monotone (λ x, Ici (f x)) :=
 antitone_Ici.comp hf
 
+protected lemma antitone_on.Ici (hf : antitone_on f s) : monotone_on (λ x, Ici (f x)) s :=
+antitone_Ici.comp_antitone_on hf
+
 protected lemma monotone.Iic (hf : monotone f) : monotone (λ x, Iic (f x)) :=
 monotone_Iic.comp hf
 
+protected lemma monotone_on.Iic (hf : monotone_on f s) : monotone_on (λ x, Iic (f x)) s :=
+monotone_Iic.comp_monotone_on hf
+
 protected lemma antitone.Iic (hf : antitone f) : antitone (λ x, Iic (f x)) :=
 monotone_Iic.comp_antitone hf
 
+protected lemma antitone_on.Iic (hf : antitone_on f s) : antitone_on (λ x, Iic (f x)) s :=
+monotone_Iic.comp_antitone_on hf
+
 protected lemma monotone.Ioi (hf : monotone f) : antitone (λ x, Ioi (f x)) :=
 antitone_Ioi.comp_monotone hf
 
+protected lemma monotone_on.Ioi (hf : monotone_on f s) : antitone_on (λ x, Ioi (f x)) s :=
+antitone_Ioi.comp_monotone_on hf
+
 protected lemma antitone.Ioi (hf : antitone f) : monotone (λ x, Ioi (f x)) :=
 antitone_Ioi.comp hf
 
+protected lemma antitone_on.Ioi (hf : antitone_on f s) : monotone_on (λ x, Ioi (f x)) s :=
+antitone_Ioi.comp_antitone_on hf
+
 protected lemma monotone.Iio (hf : monotone f) : monotone (λ x, Iio (f x)) :=
 monotone_Iio.comp hf
 
+protected lemma monotone_on.Iio (hf : monotone_on f s) : monotone_on (λ x, Iio (f x)) s :=
+monotone_Iio.comp_monotone_on hf
+
 protected lemma antitone.Iio (hf : antitone f) : antitone (λ x, Iio (f x)) :=
 monotone_Iio.comp_antitone hf
 
+protected lemma antitone_on.Iio (hf : antitone_on f s) : antitone_on (λ x, Iio (f x)) s :=
+monotone_Iio.comp_antitone_on 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 monotone_on.Icc (hf : monotone_on f s) (hg : antitone_on g s) :
+  antitone_on (λ x, Icc (f x) (g x)) s :=
+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 antitone_on.Icc (hf : antitone_on f s) (hg : monotone_on g s) :
+  monotone_on (λ x, Icc (f x) (g x)) s :=
+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 monotone_on.Ico (hf : monotone_on f s) (hg : antitone_on g s) :
+  antitone_on (λ x, Ico (f x) (g x)) s :=
+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 antitone_on.Ico (hf : antitone_on f s) (hg : monotone_on g s) :
+  monotone_on (λ x, Ico (f x) (g x)) s :=
+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 monotone_on.Ioc (hf : monotone_on f s) (hg : antitone_on g s) :
+  antitone_on (λ x, Ioc (f x) (g x)) s :=
+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 antitone_on.Ioc (hf : antitone_on f s) (hg : monotone_on g s) :
+  monotone_on (λ x, Ioc (f x) (g x)) s :=
+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 monotone_on.Ioo (hf : monotone_on f s) (hg : antitone_on g s) :
+  antitone_on (λ x, Ioo (f x) (g x)) s :=
+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
 
+protected lemma antitone_on.Ioo (hf : antitone_on f s) (hg : monotone_on g s) :
+  monotone_on (λ x, Ioo (f x) (g x)) s :=
+hf.Ioi.inter hg.Iio
+
 end Ixx
 
 section Union

src/data/set/lattice.lean

@@ -135,18 +135,34 @@ theorem _root_.monotone.inter [preorder β] {f g : β → set α}
   (hf : monotone f) (hg : monotone g) : monotone (λ x, f x ∩ g x) :=
 hf.inf hg
 
+theorem _root_.monotone_on.inter [preorder β] {f g : β → set α} {s : set β}
+  (hf : monotone_on f s) (hg : monotone_on g s) : monotone_on (λ x, f x ∩ g x) s :=
+hf.inf hg
+
 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_.antitone_on.inter [preorder β] {f g : β → set α} {s : set β}
+  (hf : antitone_on f s) (hg : antitone_on g s) : antitone_on (λ x, f x ∩ g x) s :=
+hf.inf hg
+
 theorem _root_.monotone.union [preorder β] {f g : β → set α}
   (hf : monotone f) (hg : monotone g) : monotone (λ x, f x ∪ g x) :=
 hf.sup hg
 
+theorem _root_.monotone_on.union [preorder β] {f g : β → set α} {s : set β}
+  (hf : monotone_on f s) (hg : monotone_on g s) : monotone_on (λ x, f x ∪ g x) s :=
+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 _root_.antitone_on.union [preorder β] {f g : β → set α} {s : set β}
+  (hf : antitone_on f s) (hg : antitone_on g s) : antitone_on (λ x, f x ∪ g x) s :=
+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
@@ -1260,12 +1276,6 @@ end preimage
 
 section prod
 
-theorem monotone_prod [preorder α] {f : α → set β} {g : α → set γ}
-  (hf : monotone f) (hg : monotone g) : monotone (λ x, f x ×ˢ g x) :=
-λ a b h, prod_mono (hf h) (hg h)
-
-alias monotone_prod ← monotone.set_prod
-
 lemma prod_Union {s : set α} {t : ι → set β} : s ×ˢ (⋃ i, t i) = ⋃ i, s ×ˢ (t i) := by { ext, simp }
 
 lemma prod_Union₂ {s : set α} {t : Π i, κ i → set β} : s ×ˢ (⋃ i j, t i j) = ⋃ i j, s ×ˢ t i j :=
@@ -1299,7 +1309,6 @@ end
 
 end prod
 
-
 section image2
 
 variables (f : α → β → γ) {s : set α} {t : set β}

src/data/set/prod.lean

@@ -255,6 +255,26 @@ set.ext $ λ a,
 
 @[simp] lemma image2_mk_eq_prod : image2 prod.mk s t = s ×ˢ t := ext $ by simp
 
+section mono
+
+variables [preorder α] {f : α → set β} {g : α → set γ}
+
+theorem _root_.monotone.set_prod (hf : monotone f) (hg : monotone g) : monotone (λ x, f x ×ˢ g x) :=
+λ a b h, prod_mono (hf h) (hg h)
+
+theorem _root_.antitone.set_prod (hf : antitone f) (hg : antitone g) : antitone (λ x, f x ×ˢ g x) :=
+λ a b h, prod_mono (hf h) (hg h)
+
+theorem _root_.monotone_on.set_prod (hf : monotone_on f s) (hg : monotone_on g s) :
+  monotone_on (λ x, f x ×ˢ g x) s :=
+λ a ha b hb h, prod_mono (hf ha hb h) (hg ha hb h)
+
+theorem _root_.antitone_on.set_prod (hf : antitone_on f s) (hg : antitone_on g s) :
+  antitone_on (λ x, f x ×ˢ g x) s :=
+λ a ha b hb h, prod_mono (hf ha hb h) (hg ha hb h)
+
+end mono
+
 end prod
 
 /-! ### Diagonal -/

src/order/filter/lift.lean

@@ -390,14 +390,13 @@ begin
 end
 
 lemma prod_same_eq : f ×ᶠ f = f.lift' (λ t : set α, t ×ˢ t) :=
-by rw [prod_def];
-from lift_lift'_same_eq_lift'
-  (assume s, set.monotone_prod monotone_const monotone_id)
-  (assume t, set.monotone_prod monotone_id monotone_const)
+prod_def.trans $ lift_lift'_same_eq_lift'
+  (λ s, monotone_const.set_prod monotone_id)
+  (λ t, monotone_id.set_prod monotone_const)
 
 lemma mem_prod_same_iff {s : set (α×α)} :
   s ∈ f ×ᶠ f ↔ (∃t∈f, t ×ˢ t ⊆ s) :=
-by rw [prod_same_eq, mem_lift'_sets]; exact set.monotone_prod monotone_id monotone_id
+by { rw [prod_same_eq, mem_lift'_sets], exact monotone_id.set_prod monotone_id }
 
 lemma tendsto_prod_self_iff {f : α × α → β} {x : filter α} {y : filter β} :
   filter.tendsto f (x ×ᶠ x) y ↔
@@ -411,30 +410,21 @@ lemma prod_lift_lift
   (hg₁ : monotone g₁) (hg₂ : monotone g₂) :
   (f₁.lift g₁) ×ᶠ (f₂.lift g₂) = f₁.lift (λs, f₂.lift (λt, g₁ s ×ᶠ g₂ t)) :=
 begin
-  simp only [prod_def],
-  rw [lift_assoc],
+  simp only [prod_def, lift_assoc hg₁],
   apply congr_arg, funext x,
   rw [lift_comm],
   apply congr_arg, funext y,
-  rw [lift'_lift_assoc],
-  exact hg₂,
-  exact hg₁
+  apply lift'_lift_assoc hg₂
 end
 
 lemma prod_lift'_lift'
   {f₁ : filter α₁} {f₂ : filter α₂} {g₁ : set α₁ → set β₁} {g₂ : set α₂ → set β₂}
   (hg₁ : monotone g₁) (hg₂ : monotone g₂) :
-  f₁.lift' g₁ ×ᶠ f₂.lift' g₂ = f₁.lift (λs, f₂.lift' (λt, g₁ s ×ˢ g₂ t)) :=
-begin
-  rw [prod_def, lift_lift'_assoc],
-  apply congr_arg, funext x,
-  rw [lift'_lift'_assoc],
-  exact hg₂,
-  exact set.monotone_prod monotone_const monotone_id,
-  exact hg₁,
-  exact (monotone_lift' monotone_const $ monotone_lam $
-    assume x, set.monotone_prod monotone_id monotone_const)
-end
+  f₁.lift' g₁ ×ᶠ f₂.lift' g₂ = f₁.lift (λ s, f₂.lift' (λ t, g₁ s ×ˢ g₂ t)) :=
+calc f₁.lift' g₁ ×ᶠ f₂.lift' g₂ = f₁.lift (λ s, f₂.lift (λ t, 𝓟 (g₁ s) ×ᶠ 𝓟 (g₂ t))) :
+  prod_lift_lift (monotone_principal.comp hg₁) (monotone_principal.comp hg₂)
+... = f₁.lift (λ s, f₂.lift (λ t, 𝓟 (g₁ s ×ˢ g₂ t))) :
+  by simp only [prod_principal_principal]
 
 end prod
 

src/order/lattice.lean

@@ -817,6 +817,30 @@ hf.dual.map_sup _ _
 
 end monotone
 
+namespace monotone_on
+
+/-- Pointwise supremum of two monotone functions is a monotone function. -/
+protected lemma sup [preorder α] [semilattice_sup β] {f g : α → β} {s : set α}
+  (hf : monotone_on f s) (hg : monotone_on g s) : monotone_on (f ⊔ g) s :=
+λ x hx y hy h, sup_le_sup (hf hx hy h) (hg hx hy h)
+
+/-- Pointwise infimum of two monotone functions is a monotone function. -/
+protected lemma inf [preorder α] [semilattice_inf β] {f g : α → β} {s : set α}
+  (hf : monotone_on f s) (hg : monotone_on g s) : monotone_on (f ⊓ g) s :=
+(hf.dual.sup hg.dual).dual
+
+/-- Pointwise maximum of two monotone functions is a monotone function. -/
+protected lemma max [preorder α] [linear_order β] {f g : α → β} {s : set α}
+  (hf : monotone_on f s) (hg : monotone_on g s) : monotone_on (λ x, max (f x) (g x)) s :=
+hf.sup hg
+
+/-- Pointwise minimum of two monotone functions is a monotone function. -/
+protected lemma min [preorder α] [linear_order β] {f g : α → β} {s : set α}
+  (hf : monotone_on f s) (hg : monotone_on g s) : monotone_on (λ x, min (f x) (g x)) s :=
+hf.inf hg
+
+end monotone_on
+
 namespace antitone
 
 /-- Pointwise supremum of two monotone functions is a monotone function. -/
@@ -859,6 +883,30 @@ hf.dual_right.map_inf x y
 
 end antitone
 
+namespace antitone_on
+
+/-- Pointwise supremum of two antitone functions is a antitone function. -/
+protected lemma sup [preorder α] [semilattice_sup β] {f g : α → β} {s : set α}
+  (hf : antitone_on f s) (hg : antitone_on g s) : antitone_on (f ⊔ g) s :=
+λ x hx y hy h, sup_le_sup (hf hx hy h) (hg hx hy h)
+
+/-- Pointwise infimum of two antitone functions is a antitone function. -/
+protected lemma inf [preorder α] [semilattice_inf β] {f g : α → β} {s : set α}
+  (hf : antitone_on f s) (hg : antitone_on g s) : antitone_on (f ⊓ g) s :=
+(hf.dual.sup hg.dual).dual
+
+/-- Pointwise maximum of two antitone functions is a antitone function. -/
+protected lemma max [preorder α] [linear_order β] {f g : α → β} {s : set α}
+  (hf : antitone_on f s) (hg : antitone_on g s) : antitone_on (λ x, max (f x) (g x)) s :=
+hf.sup hg
+
+/-- Pointwise minimum of two antitone functions is a antitone function. -/
+protected lemma min [preorder α] [linear_order β] {f g : α → β} {s : set α}
+  (hf : antitone_on f s) (hg : antitone_on g s) : antitone_on (λ x, min (f x) (g x)) s :=
+hf.inf hg
+
+end antitone_on
+
 /-!
 ### Products of (semi-)lattices
 -/

src/order/monotone.lean

@@ -324,18 +324,34 @@ end subsingleton
 
 lemma monotone_id [preorder α] : monotone (id : α → α) := λ a b, id
 
+lemma monotone_on_id [preorder α] {s : set α} : monotone_on id s := λ a ha b hb, id
+
 lemma strict_mono_id [preorder α] : strict_mono (id : α → α) := λ a b, id
 
+lemma strict_mono_on_id [preorder α] {s : set α} : strict_mono_on id s := λ a ha b hb, id
+
 theorem monotone_const [preorder α] [preorder β] {c : β} : monotone (λ (a : α), c) :=
-λ a b _, le_refl c
+λ a b _, le_rfl
+
+theorem monotone_on_const [preorder α] [preorder β] {c : β} {s : set α} :
+  monotone_on (λ (a : α), c) s :=
+λ a _ b _ _, le_rfl
 
 theorem antitone_const [preorder α] [preorder β] {c : β} : antitone (λ (a : α), c) :=
 λ a b _, le_refl c
 
+theorem antitone_on_const [preorder α] [preorder β] {c : β} {s : set α} :
+  antitone_on (λ (a : α), c) s :=
+λ a _ b _ _, le_rfl
+
 lemma strict_mono_of_le_iff_le [preorder α] [preorder β] {f : α → β}
   (h : ∀ x y, x ≤ y ↔ f x ≤ f y) : strict_mono f :=
 λ a b, (lt_iff_lt_of_le_iff_le' (h _ _) (h _ _)).1
 
+lemma strict_anti_of_le_iff_le [preorder α] [preorder β] {f : α → β}
+  (h : ∀ x y, x ≤ y ↔ f y ≤ f x) : strict_anti f :=
+λ a b, (lt_iff_lt_of_le_iff_le' (h _ _) (h _ _)).1
+
 lemma injective_of_lt_imp_ne [linear_order α] {f : α → β} (h : ∀ x y, x < y → f x ≠ f y) :
   injective f :=
 begin

src/tactic/monotonicity/lemmas.lean

@@ -72,7 +72,7 @@ open set
 
 attribute [mono] inter_subset_inter union_subset_union
                  sUnion_mono Union₂_mono sInter_subset_sInter Inter₂_mono
-                 image_subset preimage_mono prod_mono monotone_prod seq_mono
+                 image_subset preimage_mono prod_mono monotone.set_prod seq_mono
                  image2_subset order_embedding.monotone
 attribute [mono] upper_bounds_mono_set lower_bounds_mono_set
                  upper_bounds_mono_mem  lower_bounds_mono_mem