Zulip Chat Archive

Stream: maths

Topic: simp-ing of preimages


view this post on Zulip 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

view this post on Zulip Patrick Massot (Jul 14 2020 at 20:59):

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

view this post on Zulip Kevin Buzzard (Jul 14 2020 at 20:59):

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

view this post on Zulip Patrick Massot (Jul 14 2020 at 21:00):

Yes

view this post on Zulip 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.

view this post on Zulip Heather Macbeth (Jul 14 2020 at 21:01):

Makes sense!


Last updated: May 09 2021 at 10:11 UTC