-
Notifications
You must be signed in to change notification settings - Fork 234
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] - feat: Pairwise
and composition with an equiv
#10706
Conversation
Add a lemma about `Pairwise` being preserved by composing the arguments of the pairwise relation with an equiv. ```lean lemma EquivLike.pairwise_comp_iff {X : Type*} {Y : Type*} {F} [EquivLike F Y X] (f : F) (p : X → X → Prop) : Pairwise (fun y z ↦ p (f y) (f z)) ↔ Pairwise p := by ``` This depends on `Mathlib.Data.FunLike.Equiv` and `Mathlib.Logic.Pairwise`, neither of which imports the other, so to avoid increasing the imports of very basic files I put it in its own new file, but feel free to suggest a better location of this lemma (and to golf the proof). From AperiodicMonotilesLean.
To consider in review: do we also want variants for unbundled bijective functions, and one-way implications for unbundled injective and surjective functions and for |
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
I've now added the lemmas for unbundled functions (in |
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.
Thanks 🎉
bors merge
Add a lemma about `Pairwise` being preserved by composing the arguments of the pairwise relation with an equiv. ```lean lemma EquivLike.pairwise_comp_iff {X : Type*} {Y : Type*} {F} [EquivLike F Y X] (f : F) (p : X → X → Prop) : Pairwise (fun y z ↦ p (f y) (f z)) ↔ Pairwise p := by ``` This depends on `Mathlib.Data.FunLike.Equiv` and `Mathlib.Logic.Pairwise`, neither of which imports the other, so to avoid increasing the imports of very basic files I put it in its own new file, but feel free to suggest a better location of this lemma (and to golf the proof). From AperiodicMonotilesLean.
Pull request successfully merged into master. Build succeeded: |
Pairwise
and composition with an equivPairwise
and composition with an equiv
Add a lemma about `Pairwise` being preserved by composing the arguments of the pairwise relation with an equiv. ```lean lemma EquivLike.pairwise_comp_iff {X : Type*} {Y : Type*} {F} [EquivLike F Y X] (f : F) (p : X → X → Prop) : Pairwise (fun y z ↦ p (f y) (f z)) ↔ Pairwise p := by ``` This depends on `Mathlib.Data.FunLike.Equiv` and `Mathlib.Logic.Pairwise`, neither of which imports the other, so to avoid increasing the imports of very basic files I put it in its own new file, but feel free to suggest a better location of this lemma (and to golf the proof). From AperiodicMonotilesLean.
Add a lemma about `Pairwise` being preserved by composing the arguments of the pairwise relation with an equiv. ```lean lemma EquivLike.pairwise_comp_iff {X : Type*} {Y : Type*} {F} [EquivLike F Y X] (f : F) (p : X → X → Prop) : Pairwise (fun y z ↦ p (f y) (f z)) ↔ Pairwise p := by ``` This depends on `Mathlib.Data.FunLike.Equiv` and `Mathlib.Logic.Pairwise`, neither of which imports the other, so to avoid increasing the imports of very basic files I put it in its own new file, but feel free to suggest a better location of this lemma (and to golf the proof). From AperiodicMonotilesLean.
Add a lemma about `Pairwise` being preserved by composing the arguments of the pairwise relation with an equiv. ```lean lemma EquivLike.pairwise_comp_iff {X : Type*} {Y : Type*} {F} [EquivLike F Y X] (f : F) (p : X → X → Prop) : Pairwise (fun y z ↦ p (f y) (f z)) ↔ Pairwise p := by ``` This depends on `Mathlib.Data.FunLike.Equiv` and `Mathlib.Logic.Pairwise`, neither of which imports the other, so to avoid increasing the imports of very basic files I put it in its own new file, but feel free to suggest a better location of this lemma (and to golf the proof). From AperiodicMonotilesLean.
Add a lemma about `Pairwise` being preserved by composing the arguments of the pairwise relation with an equiv. ```lean lemma EquivLike.pairwise_comp_iff {X : Type*} {Y : Type*} {F} [EquivLike F Y X] (f : F) (p : X → X → Prop) : Pairwise (fun y z ↦ p (f y) (f z)) ↔ Pairwise p := by ``` This depends on `Mathlib.Data.FunLike.Equiv` and `Mathlib.Logic.Pairwise`, neither of which imports the other, so to avoid increasing the imports of very basic files I put it in its own new file, but feel free to suggest a better location of this lemma (and to golf the proof). From AperiodicMonotilesLean.
Add a lemma about
Pairwise
being preserved by composing the arguments of the pairwise relation with an equiv.This depends on
Mathlib.Data.FunLike.Equiv
andMathlib.Logic.Pairwise
, neither of which imports the other, so to avoid increasing the imports of very basic files I put it in its own new file, but feel free to suggest a better location of this lemma (and to golf the proof).From AperiodicMonotilesLean.