Curious about missing filter lemma variant

Stream: mathlib4

[metakuntyyy]

I have checked the filter docs and found three lemmas, that seem to have inconsistent naming conventions and appear to be missing a lemma.

https://leanprover-community.github.io/mathlib4_docs/Mathlib/Order/Filter/Map.html#Filter.map_comap
https://leanprover-community.github.io/mathlib4_docs/Mathlib/Order/Filter/Map.html#Filter.comap_map
https://leanprover-community.github.io/mathlib4_docs/Mathlib/Order/Filter/Map.html#Filter.map_comap_of_surjective

Filter.comap_map should be called Filter.comap_map_of_injective and an unconditional Filter.comap_map should be added akin to Filter.map_comap. I'd like to add the unconditional lemma but I'm not sure what the RHS is supposed to be. Does anyone have ideas?

[Aaron Liu]

The corresponding lemmas for Set are

• docs#Set.image_preimage_eq_inter_range
• docs#Set.preimage_image_eq
• docs#Set.image_preimage_eq

[Aaron Liu]

If you can find the Set version of the filter lemma you want I will gladly help you translate it into filter

[metakuntyyy]

It could be that it's impossible to define in an easier way. I tried to find it in the docs but couldn't find it.

import Mathlib

open Set

variable {α β : Type*}

theorem preimage_image_eq_question {f : α → β} {t : Set α} :
     (f ⁻¹' (f '' t)) = sorry ∩ t := by
  sorry

It appears that taking preimages before images is way better behaved that taking images before preimages. I tried it with sin. If you take the image of $\{0\}$ with sin you get all the multiple of $\pi$ but there is no way to describe this fact elementary other than take the image and then the preimage. Taking preimages of a set means you can split whether an element is in the image or not. If x is in the image then it will be included by the preimage-image operation. If x is not in the image then we have to exclude it by intersecting with Set.range f.

This is precisely what https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Set/Image.html#Set.image_preimage_eq_inter_range states.

Do I see that correctly that there can't be an elementary Set.preimage_image_eq_question because the question can't be answered in an elementary fashion? If so, that would also conclude the same result for filters.

Well I mean technically you can look at the union of singleton sets and take the union of the preimages of those singleton sets. Not sure if that makes it any simpler.

[Anatole Dedecker]

The correct statement would be that $f^{-1}(f(T))$ is the closure of $T$ under the equivalence relation induced by $f$

[metakuntyyy]

How would I write that one down?

[Patrick Massot]

I’m afraid the most concise way of saying it is $f^{-1}(f(T))$.

[Patrick Massot]

And I agree the names of those conditional lemmas are not great.