State in Lean that: if set empty, then X, else Y

Stream: new members

[An Qi Zhang]

Hello, if I have a Set s, and I wanted to define something different in the case s is empty and the case it's not empty, how would I state this in Lean?

As an example, consider if I wanted to map from s to an Option type. Here, if s is empty, I want to map to none. If it's not empty, I want to map to some element.

Here's an MWE:

import Mathlib

def Set.setToOption {α : Type} (s : Set α) : Option α :=
  -- How should I write in Lean: "if empty, then none, otherwise, then some single element"
  if IsEmpty s then -- This isn't the right way to do this
    none
  else
    -- Want to pick out one element out of `s` (axiom of choice?)
    sorry

As a side question: would this def change if I have the hypothesis that s is subsingleton? I imagine I could just use the same def?

[Ruben Van de Velde]

if h : s = \empty will work, though you might need to turn on classical logic

[An Qi Zhang]

Ah right, thanks!

[Kenny Lau]

@An Qi Zhang it might be useful to think in terms of algorithms to understand why this has to be noncomputable:

Set α gives you a true/false statement (i.e. Prop), so you can't really compute anything using it. I can embed Riemann's hypothesis inside a Prop, and there's no way you can decide if it's true or false, so basically anything concrete (i.e. Option α) you want to produce will have no algorithm for it

[Kenny Lau]

import Mathlib.Data.Set.Basic

universe u

open Classical in
noncomputable def Set.setToOption {α : Type u} (s : Set α) : Option α :=
  if h : s.Nonempty then some h.some else none

[Kenny Lau]

I would prefer using Nonempty because it seems to have more support