-
Notifications
You must be signed in to change notification settings - Fork 317
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - chore(Data/Set): split Data/Set/Function #17091
Closed
Closed
Changes from all commits
Commits
File filter
Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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 |
Oops, something went wrong.
Oops, something went wrong.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Can this be under
Order?Order.Monotone.Setmaybe?There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I'm not convinced by that name - a good chunk of the lemmas in
Order.MonotoneinvolveSetanyway, so it's not a good disambiguator. More specifically, what would be the deciding factor for a new lemma going inOrder.Monotone.Setas opposed to any one of the other files inOrder.Monotone?There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think there's little to none, which surely is an argument for putting the files close together or even merge them?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I'm not opposed to putting the files close together, I just don't think
Order.Monotone.Setis a good name for the new file!There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Order.Monotone.SetFunction? 🤷There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
More importantly, the lemmas in this file use lemmas from
Data.Set.Function, which also creates an import cycle.There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Sounds like the "right now" is very outdated
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Where? I don't see any lemma from
Data.Set.Functionbeing used. I see definitions being used, but those could move toData.Set.OperationsThere was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Unfortunately it is not just definitions that are used here, lemmas from
Data.Set.Functionare used in the file. Furthermore, even if it were only definitions being used, it is out of scope of this PR to additionally move around definitions.There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Okay, but merging was merely a suggestion for how to put the material under
Order.Monotone. Please move this new file underOrder.Monotone