Equivalence of type with an element to an option type

Stream: Is there code for X?

[Bolton Bailey]

Do we have something that, given (a : A), establishes an equivalence between A and Option {b : A // a \neq b}? I would have assumed this would be called docs#Equiv.optionSubtype, but that is something else.

[Floris van Doorn]

Isn't that Equiv.optionSubtype a |>.symm (.refl _) |>.1?

[Bolton Bailey]

does that complete the sorry here somehow?

lemma Equiv.toOption (A : Type) (a : A) [DecidableEq A] : Σ B : Type, A ≃ Option B := sorry

[Floris van Doorn]

import Mathlib.Logic.Equiv.Option

lemma Equiv.toOption (A : Type) (a : A) [DecidableEq A] : Σ B : Type, A ≃ Option B :=
  ⟨_, Equiv.optionSubtype a |>.symm (.refl _) |>.1.symm⟩

[Yaël Dillies]

We do have this directly too. Look around docs#Pointed, specifically the equivalence with docs#PartFun

[Bolton Bailey]

Yaël Dillies said:

We do have this directly too. Look around docs#Pointed, specifically the equivalence with docs#PartFun

I don't see this in that file, and the second link is broken, can you point it out?

[Bolton Bailey]

#11095 can be scrapped if this object exists somewhere

[Timo Carlin-Burns]

docs#PartialFun

[Yaël Dillies]

It's used within the categorical equivalence. Sorry I'm not at a computer