## Stream: maths

### Topic: simp-ing of preimages

#### Heather Macbeth (Jul 14 2020 at 20:58):

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 (Jul 14 2020 at 20:59):

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

#### Kevin Buzzard (Jul 14 2020 at 20:59):

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

Yes

#### Kevin Buzzard (Jul 14 2020 at 21:00):

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

#### Heather Macbeth (Jul 14 2020 at 21:01):

Makes sense!

Last updated: May 09 2021 at 10:11 UTC