Help name this def

Stream: mathlib4

[Winston Yin (尹維晨)]

For #9940, which is almost ready, how should we name the following definition?

/--
Given two sets `A` and `B`, `setRestrict A B` is the set of `↑A` formed by the elements
whose value is in `B`.
-/
open Set

namespace Subset

def setRestrict (A B : Set α) : Set ↑A := (↑) ⁻¹' B

[Notification Bot]

A message was moved here from #mathlib4 > Should Sets be coerced? by Winston Yin (尹維晨).

[Eric Wieser]

For reference, the most similar existing definition is docs#Subgroup.subgroupOf

[Winston Yin (尹維晨)]

I think we can have Set.restrictSet, so as to suggest a specialisation of docs#Set.restrict to Set. Other options are Set.restrictTo or Set.setOf, but the latter risks confusion with set builder lemmas.

[Winston Yin (尹維晨)]

@Miguel Marco

[Eric Wieser]

I don't think the connection with docs#Set.restrict is one we want to emphasize, just as we don't try to emphasize that docs#Set.preimage is a "specialization" of docs#Function.comp ! The fact that sets are functions should be considered an implementation detail

[Anatole Dedecker]

In that case I think the restriction wording is perfectly fine independently of the implementation detail though. Anything that corresponds to some pullback along an inclusion can reasonably be called a restriction imo

[Eric Wieser]

If we use Set.restrictSet(which I agree is ok), then we should probably rename Subgroup.subgroupOf to Subgroup.restrictSubgroup