Passing to subsets of a subspace

Stream: mathlib4

[Kyle Miller]

There's some inconsistency with how we go from a subset of the whole space to a subset of a subspace. I think it would be nice if s ∩ . were the way we write it, since then it's like a prefix operation, and it leads to better parallelism for (Subtype.val : s -> _) '' . lemmas.

In #10433 I did a small amount of reversing some intersections to see how much work this would be. What do we think about this?

This is motivated by #9940, which introduces scoped notation s ↓∩ . for the adjoint to (Subtype.val : s -> _) '' .. Consistency means lemmas printed with this notation can look like A ↓∩ B ⊆ A ↓∩ C ↔ A ∩ B ⊆ A ∩ C rather than A ↓∩ B ⊆ A ↓∩ C ↔ B ∩ A ⊆ C ∩ A.

[Eric Wieser]

Taking a random sample from that PR, f '' (f ⁻¹' t) = t ∩ range f does seem like a worse order than the new f '' (f ⁻¹' t) = range f ∩ t, using the heuristic "lemmas should avoid changing the order unless they have to"

[Eric Wieser]

(which is to say, I'm in broadly in favor of this change)

[Emilie (Shad Amethyst)]

"changing" here referring to the difference between the lhs and the rhs of the equality, not the change brought by the PR?

[Miguel Marco]

Which is the standard workflow in these cases (I mean, when changes relevant for a PR are implemented in another PR)?

We wait for #10433 to be merged before continuing with #9940?

[Ruben Van de Velde]

Yes, that seems to be the best approach here. You should update the summary of the PR to have a "depends on" link to the other PR; there should be an example in a html comment there