Bourbaki Note on function naming This code globally follows some of Mathlib4 conventions, namely '' for image of a set -1' for preimage of a set