Zulip Chat Archive

Stream: new members

Topic: Eliminating a set into an element


Yakov Pechersky (Oct 15 2020 at 16:53):

I have a function f : x \to option y that is injective over all the some y values in the codomain. I'm trying to define a function that retrieves the x that has f x = y, if I also know that f is surjective. I can say that {x | f x = y} for some fixed y is a subsingleton, due to the injectivity, and is nonempty, due to the surjectivity.

Is there some definition that lets me eliminate a singleton set back into the element it's made from? That is, I can (I think) show that a set that is a singleton from subsingleton and nonempty. Is there some better way of expressing this? I couldn't find a mathlib way of expressing "partially injective".

Johan Commelin (Oct 15 2020 at 17:14):

classical.some (h : s.nonempty) will give you an element of s.

Yakov Pechersky (Oct 15 2020 at 17:16):

But in a noncomputable way, correct?

Yury G. Kudryashov (Oct 15 2020 at 17:22):

There is no computable way to invert a function.

Eric Wieser (Oct 15 2020 at 17:23):

Does lean mathlib have the computable brute-force def for doing so given [fintype x]?

Yakov Pechersky (Oct 15 2020 at 17:24):

Eric's on the same thought as me

Reid Barton (Oct 15 2020 at 17:24):

You mean, "Does mathlib have ..."

Bryan Gin-ge Chen (Oct 15 2020 at 17:25):

You might need encodable as well.

Yury G. Kudryashov (Oct 15 2020 at 17:28):

Let me try docs#finset.choose

Bryan Gin-ge Chen (Oct 15 2020 at 17:28):

Oh, maybe docs#fintype.bij_inv

Adam Topaz (Oct 15 2020 at 17:28):

docs#fintype.choose I assume?


Last updated: Dec 20 2023 at 11:08 UTC