diff --git a/Mathlib.lean b/Mathlib.lean index 4de0c7bf38993..be905c4fe4ba5 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -2538,6 +2538,7 @@ import Mathlib.Data.Set.Image import Mathlib.Data.Set.Lattice import Mathlib.Data.Set.List import Mathlib.Data.Set.MemPartition +import Mathlib.Data.Set.Monotone import Mathlib.Data.Set.MulAntidiagonal import Mathlib.Data.Set.NAry import Mathlib.Data.Set.Notation diff --git a/Mathlib/Data/Int/Lemmas.lean b/Mathlib/Data/Int/Lemmas.lean index 9300c6b89865c..61ccb22c02adb 100644 --- a/Mathlib/Data/Int/Lemmas.lean +++ b/Mathlib/Data/Int/Lemmas.lean @@ -6,6 +6,7 @@ Authors: Jeremy Avigad import Mathlib.Data.Int.Bitwise import Mathlib.Data.Int.Order.Lemmas import Mathlib.Data.Set.Function +import Mathlib.Data.Set.Monotone import Mathlib.Order.Interval.Set.Basic /-! diff --git a/Mathlib/Data/Set/Function.lean b/Mathlib/Data/Set/Function.lean index e421706c65305..27b5f6c537661 100644 --- a/Mathlib/Data/Set/Function.lean +++ b/Mathlib/Data/Set/Function.lean @@ -166,8 +166,7 @@ end restrict /-! ### Equality on a set -/ section equality -variable {s s₁ s₂ : Set α} {t t₁ t₂ : Set β} {p : Set γ} {f f₁ f₂ f₃ : α → β} {g g₁ g₂ : β → γ} - {f' f₁' f₂' : β → α} {g' : γ → β} {a : α} {b : β} +variable {s s₁ s₂ : Set α} {f₁ f₂ f₃ : α → β} {g : β → γ} {a : α} @[simp] theorem eqOn_empty (f₁ f₂ : α → β) : EqOn f₁ f₂ ∅ := fun _ => False.elim @@ -233,78 +232,7 @@ alias ⟨EqOn.comp_eq, _⟩ := eqOn_range end equality -/-! ### Congruence lemmas for monotonicity and antitonicity -/ -section Order - -variable {s : Set α} {f₁ f₂ : α → β} [Preorder α] [Preorder β] - -theorem _root_.MonotoneOn.congr (h₁ : MonotoneOn f₁ s) (h : s.EqOn f₁ f₂) : MonotoneOn f₂ s := by - intro a ha b hb hab - rw [← h ha, ← h hb] - exact h₁ ha hb hab - -theorem _root_.AntitoneOn.congr (h₁ : AntitoneOn f₁ s) (h : s.EqOn f₁ f₂) : AntitoneOn f₂ s := - h₁.dual_right.congr h - -theorem _root_.StrictMonoOn.congr (h₁ : StrictMonoOn f₁ s) (h : s.EqOn f₁ f₂) : - StrictMonoOn f₂ s := by - intro a ha b hb hab - rw [← h ha, ← h hb] - exact h₁ ha hb hab - -theorem _root_.StrictAntiOn.congr (h₁ : StrictAntiOn f₁ s) (h : s.EqOn f₁ f₂) : StrictAntiOn f₂ s := - h₁.dual_right.congr h - -theorem EqOn.congr_monotoneOn (h : s.EqOn f₁ f₂) : MonotoneOn f₁ s ↔ MonotoneOn f₂ s := - ⟨fun h₁ => h₁.congr h, fun h₂ => h₂.congr h.symm⟩ - -theorem EqOn.congr_antitoneOn (h : s.EqOn f₁ f₂) : AntitoneOn f₁ s ↔ AntitoneOn f₂ s := - ⟨fun h₁ => h₁.congr h, fun h₂ => h₂.congr h.symm⟩ - -theorem EqOn.congr_strictMonoOn (h : s.EqOn f₁ f₂) : StrictMonoOn f₁ s ↔ StrictMonoOn f₂ s := - ⟨fun h₁ => h₁.congr h, fun h₂ => h₂.congr h.symm⟩ - -theorem EqOn.congr_strictAntiOn (h : s.EqOn f₁ f₂) : StrictAntiOn f₁ s ↔ StrictAntiOn f₂ s := - ⟨fun h₁ => h₁.congr h, fun h₂ => h₂.congr h.symm⟩ - -end Order - -/-! ### Monotonicity lemmas -/ -section Mono - -variable {s s₁ s₂ : Set α} {f f₁ f₂ : α → β} [Preorder α] [Preorder β] - -theorem _root_.MonotoneOn.mono (h : MonotoneOn f s) (h' : s₂ ⊆ s) : MonotoneOn f s₂ := - fun _ hx _ hy => h (h' hx) (h' hy) - -theorem _root_.AntitoneOn.mono (h : AntitoneOn f s) (h' : s₂ ⊆ s) : AntitoneOn f s₂ := - fun _ hx _ hy => h (h' hx) (h' hy) - -theorem _root_.StrictMonoOn.mono (h : StrictMonoOn f s) (h' : s₂ ⊆ s) : StrictMonoOn f s₂ := - fun _ hx _ hy => h (h' hx) (h' hy) - -theorem _root_.StrictAntiOn.mono (h : StrictAntiOn f s) (h' : s₂ ⊆ s) : StrictAntiOn f s₂ := - fun _ hx _ hy => h (h' hx) (h' hy) - -protected theorem _root_.MonotoneOn.monotone (h : MonotoneOn f s) : - Monotone (f ∘ Subtype.val : s → β) := - fun x y hle => h x.coe_prop y.coe_prop hle - -protected theorem _root_.AntitoneOn.monotone (h : AntitoneOn f s) : - Antitone (f ∘ Subtype.val : s → β) := - fun x y hle => h x.coe_prop y.coe_prop hle - -protected theorem _root_.StrictMonoOn.strictMono (h : StrictMonoOn f s) : - StrictMono (f ∘ Subtype.val : s → β) := - fun x y hlt => h x.coe_prop y.coe_prop hlt - -protected theorem _root_.StrictAntiOn.strictAnti (h : StrictAntiOn f s) : - StrictAnti (f ∘ Subtype.val : s → β) := - fun x y hlt => h x.coe_prop y.coe_prop hlt - -end Mono - -variable {s s₁ s₂ : Set α} {t t₁ t₂ : Set β} {p : Set γ} {f f₁ f₂ f₃ : α → β} {g g₁ g₂ : β → γ} +variable {s s₁ s₂ : Set α} {t t₁ t₂ : Set β} {p : Set γ} {f f₁ f₂ : α → β} {g g₁ g₂ : β → γ} {f' f₁' f₂' : β → α} {g' : γ → β} {a : α} {b : β} section MapsTo @@ -521,8 +449,6 @@ theorem preimage_restrictPreimage {u : Set t} : rw [← preimage_preimage (g := f) (f := Subtype.val), ← image_val_preimage_restrictPreimage, preimage_image_eq _ Subtype.val_injective] -variable {U : ι → Set β} - lemma restrictPreimage_injective (hf : Injective f) : Injective (t.restrictPreimage f) := fun _ _ e => Subtype.coe_injective <| hf <| Subtype.mk.inj e @@ -1331,23 +1257,6 @@ lemma bijOn_comm {g : β → α} (h : InvOn f g t s) : BijOn f s t ↔ BijOn g t end Set -/-! ### Monotone -/ -namespace Monotone - -variable [Preorder α] [Preorder β] {f : α → β} - -protected theorem restrict (h : Monotone f) (s : Set α) : Monotone (s.restrict f) := fun _ _ hxy => - h hxy - -protected theorem codRestrict (h : Monotone f) {s : Set β} (hs : ∀ x, f x ∈ s) : - Monotone (s.codRestrict f hs) := - h - -protected theorem rangeFactorization (h : Monotone f) : Monotone (Set.rangeFactorization f) := - h - -end Monotone - /-! ### Piecewise defined function -/ namespace Set @@ -1370,10 +1279,6 @@ theorem piecewise_insert_self {j : α} [∀ i, Decidable (i ∈ insert j s)] : variable [∀ j, Decidable (j ∈ s)] --- TODO: move! -instance Compl.decidableMem (j : α) : Decidable (j ∈ sᶜ) := - instDecidableNot - theorem piecewise_insert [DecidableEq α] (j : α) [∀ i, Decidable (i ∈ insert j s)] : (insert j s).piecewise f g = Function.update (s.piecewise f g) j (f j) := by simp (config := { unfoldPartialApp := true }) only [piecewise, mem_insert_iff] @@ -1513,46 +1418,6 @@ theorem univ_pi_piecewise_univ {ι : Type*} {α : ι → Type*} (s : Set ι) (t end Set -section strictMono - -theorem StrictMonoOn.injOn [LinearOrder α] [Preorder β] {f : α → β} {s : Set α} - (H : StrictMonoOn f s) : s.InjOn f := fun x hx y hy hxy => - show Ordering.eq.Compares x y from (H.compares hx hy).1 hxy - -theorem StrictAntiOn.injOn [LinearOrder α] [Preorder β] {f : α → β} {s : Set α} - (H : StrictAntiOn f s) : s.InjOn f := - @StrictMonoOn.injOn α βᵒᵈ _ _ f s H - -theorem StrictMonoOn.comp [Preorder α] [Preorder β] [Preorder γ] {g : β → γ} {f : α → β} {s : Set α} - {t : Set β} (hg : StrictMonoOn g t) (hf : StrictMonoOn f s) (hs : Set.MapsTo f s t) : - StrictMonoOn (g ∘ f) s := fun _x hx _y hy hxy => hg (hs hx) (hs hy) <| hf hx hy hxy - -theorem StrictMonoOn.comp_strictAntiOn [Preorder α] [Preorder β] [Preorder γ] {g : β → γ} - {f : α → β} {s : Set α} {t : Set β} (hg : StrictMonoOn g t) (hf : StrictAntiOn f s) - (hs : Set.MapsTo f s t) : StrictAntiOn (g ∘ f) s := fun _x hx _y hy hxy => - hg (hs hy) (hs hx) <| hf hx hy hxy - -theorem StrictAntiOn.comp [Preorder α] [Preorder β] [Preorder γ] {g : β → γ} {f : α → β} {s : Set α} - {t : Set β} (hg : StrictAntiOn g t) (hf : StrictAntiOn f s) (hs : Set.MapsTo f s t) : - StrictMonoOn (g ∘ f) s := fun _x hx _y hy hxy => hg (hs hy) (hs hx) <| hf hx hy hxy - -theorem StrictAntiOn.comp_strictMonoOn [Preorder α] [Preorder β] [Preorder γ] {g : β → γ} - {f : α → β} {s : Set α} {t : Set β} (hg : StrictAntiOn g t) (hf : StrictMonoOn f s) - (hs : Set.MapsTo f s t) : StrictAntiOn (g ∘ f) s := fun _x hx _y hy hxy => - hg (hs hx) (hs hy) <| hf hx hy hxy - -@[simp] -theorem strictMono_restrict [Preorder α] [Preorder β] {f : α → β} {s : Set α} : - StrictMono (s.restrict f) ↔ StrictMonoOn f s := by simp [Set.restrict, StrictMono, StrictMonoOn] - -alias ⟨_root_.StrictMono.of_restrict, _root_.StrictMonoOn.restrict⟩ := strictMono_restrict - -theorem StrictMono.codRestrict [Preorder α] [Preorder β] {f : α → β} (hf : StrictMono f) - {s : Set β} (hs : ∀ x, f x ∈ s) : StrictMono (Set.codRestrict f s hs) := - hf - -end strictMono - namespace Function open Set @@ -1640,22 +1505,6 @@ theorem update_comp_eq_of_not_mem_range {α : Sort*} {β : Type*} {γ : Sort*} [ theorem insert_injOn (s : Set α) : sᶜ.InjOn fun a => insert a s := fun _a ha _ _ => (insert_inj ha).1 -theorem monotoneOn_of_rightInvOn_of_mapsTo {α β : Type*} [PartialOrder α] [LinearOrder β] - {φ : β → α} {ψ : α → β} {t : Set β} {s : Set α} (hφ : MonotoneOn φ t) - (φψs : Set.RightInvOn ψ φ s) (ψts : Set.MapsTo ψ s t) : MonotoneOn ψ s := by - rintro x xs y ys l - rcases le_total (ψ x) (ψ y) with (ψxy|ψyx) - · exact ψxy - · have := hφ (ψts ys) (ψts xs) ψyx - rw [φψs.eq ys, φψs.eq xs] at this - induction le_antisymm l this - exact le_refl _ - -theorem antitoneOn_of_rightInvOn_of_mapsTo [PartialOrder α] [LinearOrder β] - {φ : β → α} {ψ : α → β} {t : Set β} {s : Set α} (hφ : AntitoneOn φ t) - (φψs : Set.RightInvOn ψ φ s) (ψts : Set.MapsTo ψ s t) : AntitoneOn ψ s := - (monotoneOn_of_rightInvOn_of_mapsTo hφ.dual_left φψs ψts).dual_right - lemma apply_eq_of_range_eq_singleton {f : α → β} {b : β} (h : range f = {b}) (a : α) : f a = b := by simpa only [h, mem_singleton_iff] using mem_range_self (f := f) a @@ -1765,4 +1614,4 @@ lemma bijOn_swap (ha : a ∈ s) (hb : b ∈ s) : BijOn (swap a b) s s := end Equiv -set_option linter.style.longFile 1900 +set_option linter.style.longFile 1800 diff --git a/Mathlib/Data/Set/Monotone.lean b/Mathlib/Data/Set/Monotone.lean new file mode 100644 index 0000000000000..f811b7ae15131 --- /dev/null +++ b/Mathlib/Data/Set/Monotone.lean @@ -0,0 +1,173 @@ +/- +Copyright (c) 2014 Jeremy Avigad. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Jeremy Avigad, Andrew Zipperer, Haitao Zhang, Minchao Wu, Yury Kudryashov +-/ +import Mathlib.Data.Set.Function + +/-! +# Monotone functions over sets +-/ + +variable {α β γ : Type*} + +open Equiv Equiv.Perm Function + +namespace Set + + +/-! ### Congruence lemmas for monotonicity and antitonicity -/ +section Order + +variable {s : Set α} {f₁ f₂ : α → β} [Preorder α] [Preorder β] + +theorem _root_.MonotoneOn.congr (h₁ : MonotoneOn f₁ s) (h : s.EqOn f₁ f₂) : MonotoneOn f₂ s := by + intro a ha b hb hab + rw [← h ha, ← h hb] + exact h₁ ha hb hab + +theorem _root_.AntitoneOn.congr (h₁ : AntitoneOn f₁ s) (h : s.EqOn f₁ f₂) : AntitoneOn f₂ s := + h₁.dual_right.congr h + +theorem _root_.StrictMonoOn.congr (h₁ : StrictMonoOn f₁ s) (h : s.EqOn f₁ f₂) : + StrictMonoOn f₂ s := by + intro a ha b hb hab + rw [← h ha, ← h hb] + exact h₁ ha hb hab + +theorem _root_.StrictAntiOn.congr (h₁ : StrictAntiOn f₁ s) (h : s.EqOn f₁ f₂) : StrictAntiOn f₂ s := + h₁.dual_right.congr h + +theorem EqOn.congr_monotoneOn (h : s.EqOn f₁ f₂) : MonotoneOn f₁ s ↔ MonotoneOn f₂ s := + ⟨fun h₁ => h₁.congr h, fun h₂ => h₂.congr h.symm⟩ + +theorem EqOn.congr_antitoneOn (h : s.EqOn f₁ f₂) : AntitoneOn f₁ s ↔ AntitoneOn f₂ s := + ⟨fun h₁ => h₁.congr h, fun h₂ => h₂.congr h.symm⟩ + +theorem EqOn.congr_strictMonoOn (h : s.EqOn f₁ f₂) : StrictMonoOn f₁ s ↔ StrictMonoOn f₂ s := + ⟨fun h₁ => h₁.congr h, fun h₂ => h₂.congr h.symm⟩ + +theorem EqOn.congr_strictAntiOn (h : s.EqOn f₁ f₂) : StrictAntiOn f₁ s ↔ StrictAntiOn f₂ s := + ⟨fun h₁ => h₁.congr h, fun h₂ => h₂.congr h.symm⟩ + +end Order + +/-! ### Monotonicity lemmas -/ +section Mono + +variable {s s₂ : Set α} {f : α → β} [Preorder α] [Preorder β] + +theorem _root_.MonotoneOn.mono (h : MonotoneOn f s) (h' : s₂ ⊆ s) : MonotoneOn f s₂ := + fun _ hx _ hy => h (h' hx) (h' hy) + +theorem _root_.AntitoneOn.mono (h : AntitoneOn f s) (h' : s₂ ⊆ s) : AntitoneOn f s₂ := + fun _ hx _ hy => h (h' hx) (h' hy) + +theorem _root_.StrictMonoOn.mono (h : StrictMonoOn f s) (h' : s₂ ⊆ s) : StrictMonoOn f s₂ := + fun _ hx _ hy => h (h' hx) (h' hy) + +theorem _root_.StrictAntiOn.mono (h : StrictAntiOn f s) (h' : s₂ ⊆ s) : StrictAntiOn f s₂ := + fun _ hx _ hy => h (h' hx) (h' hy) + +protected theorem _root_.MonotoneOn.monotone (h : MonotoneOn f s) : + Monotone (f ∘ Subtype.val : s → β) := + fun x y hle => h x.coe_prop y.coe_prop hle + +protected theorem _root_.AntitoneOn.monotone (h : AntitoneOn f s) : + Antitone (f ∘ Subtype.val : s → β) := + fun x y hle => h x.coe_prop y.coe_prop hle + +protected theorem _root_.StrictMonoOn.strictMono (h : StrictMonoOn f s) : + StrictMono (f ∘ Subtype.val : s → β) := + fun x y hlt => h x.coe_prop y.coe_prop hlt + +protected theorem _root_.StrictAntiOn.strictAnti (h : StrictAntiOn f s) : + StrictAnti (f ∘ Subtype.val : s → β) := + fun x y hlt => h x.coe_prop y.coe_prop hlt + +end Mono + +end Set + + + +open Function + +/-! ### Monotone -/ +namespace Monotone + +variable [Preorder α] [Preorder β] {f : α → β} + +protected theorem restrict (h : Monotone f) (s : Set α) : Monotone (s.restrict f) := fun _ _ hxy => + h hxy + +protected theorem codRestrict (h : Monotone f) {s : Set β} (hs : ∀ x, f x ∈ s) : + Monotone (s.codRestrict f hs) := + h + +protected theorem rangeFactorization (h : Monotone f) : Monotone (Set.rangeFactorization f) := + h + +end Monotone + +section strictMono + +theorem StrictMonoOn.injOn [LinearOrder α] [Preorder β] {f : α → β} {s : Set α} + (H : StrictMonoOn f s) : s.InjOn f := fun x hx y hy hxy => + show Ordering.eq.Compares x y from (H.compares hx hy).1 hxy + +theorem StrictAntiOn.injOn [LinearOrder α] [Preorder β] {f : α → β} {s : Set α} + (H : StrictAntiOn f s) : s.InjOn f := + @StrictMonoOn.injOn α βᵒᵈ _ _ f s H + +theorem StrictMonoOn.comp [Preorder α] [Preorder β] [Preorder γ] {g : β → γ} {f : α → β} {s : Set α} + {t : Set β} (hg : StrictMonoOn g t) (hf : StrictMonoOn f s) (hs : Set.MapsTo f s t) : + StrictMonoOn (g ∘ f) s := fun _x hx _y hy hxy => hg (hs hx) (hs hy) <| hf hx hy hxy + +theorem StrictMonoOn.comp_strictAntiOn [Preorder α] [Preorder β] [Preorder γ] {g : β → γ} + {f : α → β} {s : Set α} {t : Set β} (hg : StrictMonoOn g t) (hf : StrictAntiOn f s) + (hs : Set.MapsTo f s t) : StrictAntiOn (g ∘ f) s := fun _x hx _y hy hxy => + hg (hs hy) (hs hx) <| hf hx hy hxy + +theorem StrictAntiOn.comp [Preorder α] [Preorder β] [Preorder γ] {g : β → γ} {f : α → β} {s : Set α} + {t : Set β} (hg : StrictAntiOn g t) (hf : StrictAntiOn f s) (hs : Set.MapsTo f s t) : + StrictMonoOn (g ∘ f) s := fun _x hx _y hy hxy => hg (hs hy) (hs hx) <| hf hx hy hxy + +theorem StrictAntiOn.comp_strictMonoOn [Preorder α] [Preorder β] [Preorder γ] {g : β → γ} + {f : α → β} {s : Set α} {t : Set β} (hg : StrictAntiOn g t) (hf : StrictMonoOn f s) + (hs : Set.MapsTo f s t) : StrictAntiOn (g ∘ f) s := fun _x hx _y hy hxy => + hg (hs hx) (hs hy) <| hf hx hy hxy + +@[simp] +theorem strictMono_restrict [Preorder α] [Preorder β] {f : α → β} {s : Set α} : + StrictMono (s.restrict f) ↔ StrictMonoOn f s := by simp [Set.restrict, StrictMono, StrictMonoOn] + +alias ⟨_root_.StrictMono.of_restrict, _root_.StrictMonoOn.restrict⟩ := strictMono_restrict + +theorem StrictMono.codRestrict [Preorder α] [Preorder β] {f : α → β} (hf : StrictMono f) + {s : Set β} (hs : ∀ x, f x ∈ s) : StrictMono (Set.codRestrict f s hs) := + hf + +end strictMono + +namespace Function + +open Set + +theorem monotoneOn_of_rightInvOn_of_mapsTo {α β : Type*} [PartialOrder α] [LinearOrder β] + {φ : β → α} {ψ : α → β} {t : Set β} {s : Set α} (hφ : MonotoneOn φ t) + (φψs : Set.RightInvOn ψ φ s) (ψts : Set.MapsTo ψ s t) : MonotoneOn ψ s := by + rintro x xs y ys l + rcases le_total (ψ x) (ψ y) with (ψxy|ψyx) + · exact ψxy + · have := hφ (ψts ys) (ψts xs) ψyx + rw [φψs.eq ys, φψs.eq xs] at this + induction le_antisymm l this + exact le_refl _ + +theorem antitoneOn_of_rightInvOn_of_mapsTo [PartialOrder α] [LinearOrder β] + {φ : β → α} {ψ : α → β} {t : Set β} {s : Set α} (hφ : AntitoneOn φ t) + (φψs : Set.RightInvOn ψ φ s) (ψts : Set.MapsTo ψ s t) : AntitoneOn ψ s := + (monotoneOn_of_rightInvOn_of_mapsTo hφ.dual_left φψs ψts).dual_right + +end Function diff --git a/Mathlib/Order/Hom/Set.lean b/Mathlib/Order/Hom/Set.lean index 5017a61157aee..96809de232fb1 100644 --- a/Mathlib/Order/Hom/Set.lean +++ b/Mathlib/Order/Hom/Set.lean @@ -5,6 +5,7 @@ Authors: Johan Commelin -/ import Mathlib.Order.Hom.Basic import Mathlib.Logic.Equiv.Set +import Mathlib.Data.Set.Monotone import Mathlib.Data.Set.Image import Mathlib.Order.WellFounded