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] - refactor: prefer s ∩ .
when passing to a subset of s
#10433
Conversation
This is partial work to make `Subtype.val '' .` and `s ∩ .` be consistently used as adjoint operators for passing to and from a "subspace".
@@ -1679,7 +1679,7 @@ theorem mem_subgroupOf {H K : Subgroup G} {h : K} : h ∈ H.subgroupOf K ↔ (h | |||
|
|||
@[to_additive (attr := simp)] | |||
theorem subgroupOf_map_subtype (H K : Subgroup G) : (H.subgroupOf K).map K.subtype = H ⊓ K := |
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.
Arguably this should flip too
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 added a TODO
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.
It seems to me that this convention is introducing more inter_comm
s than that it removes. Wouldn't it be more ergonomical to put s
in the RHS slot?
Can you edit the description to link to the Zulip thread, @kmill? |
@jcommelin I only did fixups -- inserting
Why? |
The diff suggests to me that you would need to do fewer fixups. |
@kmill privately explained to me that he would like "passing to a subset" to behave more like a prefix operator. Which I think is a good reason. So then this is the order it should be. bors merge |
This is partial work to make `s ∩ .` be consistently used for passing to a subset of `s`. This is sort of an adjoint to `(Subtype.val : s -> _) '' .`, except for the fact that it does not produce a `Set s`. The main API changes are to `Subtype.image_preimage_val` and `Subtype.preimage_val_eq_preimage_val_iff` in `Mathlib.Data.Set.Image`. Changes in other modules are all proof fixups. [Zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Passing.20to.20subsets.20of.20a.20subspace/near/420917406)
Pull request successfully merged into master. Build succeeded: |
s ∩ .
when passing to a subset of s
s ∩ .
when passing to a subset of s
This is partial work to make `s ∩ .` be consistently used for passing to a subset of `s`. This is sort of an adjoint to `(Subtype.val : s -> _) '' .`, except for the fact that it does not produce a `Set s`. The main API changes are to `Subtype.image_preimage_val` and `Subtype.preimage_val_eq_preimage_val_iff` in `Mathlib.Data.Set.Image`. Changes in other modules are all proof fixups. [Zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Passing.20to.20subsets.20of.20a.20subspace/near/420917406)
This is partial work to make `s ∩ .` be consistently used for passing to a subset of `s`. This is sort of an adjoint to `(Subtype.val : s -> _) '' .`, except for the fact that it does not produce a `Set s`. The main API changes are to `Subtype.image_preimage_val` and `Subtype.preimage_val_eq_preimage_val_iff` in `Mathlib.Data.Set.Image`. Changes in other modules are all proof fixups. [Zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Passing.20to.20subsets.20of.20a.20subspace/near/420917406)
This is partial work to make
s ∩ .
be consistently used for passing to a subset ofs
. This is sort of an adjoint to(Subtype.val : s -> _) '' .
, except for the fact that it does not produce aSet s
.The main API changes are to
Subtype.image_preimage_val
andSubtype.preimage_val_eq_preimage_val_iff
inMathlib.Data.Set.Image
. Changes in other modules are all proof fixups.Zulip discussion