simp-ing of preimages

Stream: maths

[Heather Macbeth]

The lemma docs#set.mem_preimage is a simp lemma,

@[simp] theorem mem_preimage {s : set β} {a : α} : (a ∈ f ⁻¹' s) ↔ (f a ∈ s) := iff.rfl

If I understand correctly, this means that a ∈ f ⁻¹' s is simplified to f a ∈ s. Given this discussion yesterday about the superior simp properties of preimages, would it be better to reverse the equality so that f a ∈ s is simplified to a ∈ f ⁻¹' s? @Patrick Massot @Sebastien Gouezel

[Patrick Massot]

Preimage has better properties that direct image of sets but not direct image of points.

[Kevin Buzzard]

The bad one is f ''. Maybe f a \in s is fine

[Patrick Massot]

Yes

[Kevin Buzzard]

f '' has some embedded \exists in. id \-1' U = U is rfl but id '' U = U is not.

[Heather Macbeth]

Makes sense!