filter.mem_map

Stream: maths

[Nicolò Cavalleri]

Is there any reason that mem_map is in mathlib in this form

@[simp] lemma mem_map : t ∈ map m f ↔ {x | m x ∈ t} ∈ f := iff.rfl

and not in this form

@[simp] lemma mem_map : t ∈ map m f ↔ m ⁻¹' t ∈ f := iff.rfl

?

[Yakov Pechersky]

Does set.preimage work here?

[Patrick Massot]

This is not the type of t

[Patrick Massot]

I don't see any reason why this lemma should be stated like that.

[Patrick Massot]

You should try to change it and see whether it breaks anything

[Yakov Pechersky]

Ah yes, t : \beta. And I bet it would not work because t is not a set _

[Yakov Pechersky]

You could try m ⁻¹' {t}?

[Patrick Massot]

Why do you say t is not a set?

[Yakov Pechersky]

But I bet the simp-normal form is the one as it is stated

[Yakov Pechersky]

Patrick, you are again correct, and I am confused.

[Nicolò Cavalleri]

Patrick Massot said:

I don't see any reason why this lemma should be stated like that.

Like what sorry? You don't see why it is how it is or why it should be how I want it?

[Patrick Massot]

I don't why it is stated the way it's currently stated. Maybe this isn't clearer. I mean I agree with you.

[Nicolò Cavalleri]

Ok thanks I will PR then