Zulip Chat Archive

Stream: general

Topic: fibre of a map

Kenny Lau (Apr 16 2018 at 07:37):

I wish we have preimage of a point, whatever its use is

Mario Carneiro (Apr 16 2018 at 07:47):

Why not use f ⁻¹' {x}?

Kenny Lau (Apr 16 2018 at 07:48):

because they don't defintionally expand well

Mario Carneiro (Apr 16 2018 at 07:58):

it doesn't expand any worse than {x} itself does. Just make a simp lemma (but actually the existing simp lemmas should compose to get what you want)

Kenny Lau (Apr 16 2018 at 07:59):

that isn't definitional expansion

Kenny Lau (Apr 16 2018 at 07:59):

I mean {x} doesn't expand well

Mario Carneiro (Apr 16 2018 at 07:59):

so?

Kenny Lau (Apr 16 2018 at 07:59):

so I don't like it

Kenny Lau (Apr 16 2018 at 07:59):

nao gosto isso

Mario Carneiro (Apr 16 2018 at 08:00):

It is conceivable that we can change the definition there but it doesn't affect whether to have a definition of fiber

Kenny Lau (Apr 16 2018 at 08:02):

ok, let's just change the definition of singleton then

Last updated: Dec 20 2023 at 11:08 UTC