## Stream: general

### Topic: set.indefinite_description

#### Kenny Lau (Dec 04 2018 at 22:27):

Is it possible to fill in this sorry?

universes u
protected def set.indefinite_description {α : Type u}
{p : set α → Prop} (h : ∃ s, p s) : { s : set α // p s} := sorry


#### Reid Barton (Dec 04 2018 at 22:36):

I guess you mean without adding noncomputable? Interesting question

#### Mario Carneiro (Dec 05 2018 at 00:04):

yes

universes u
protected def set.indefinite_description {α : Type u}
{p : set α → Prop} (h : ∃ s, p s) : { s : set α // p s} :=
⟨{x : α | x ∈ classical.some h}, classical.some_spec h⟩


#### Mario Carneiro (Dec 05 2018 at 00:04):

I've mentioned before about "trivially computable" types, which includes subtypes of functions returning Prop

#### Mario Carneiro (Dec 05 2018 at 00:05):

Any term of such a type can be made computable with appropriate wrapping

#### Mario Carneiro (Dec 05 2018 at 00:06):

If you meant "without axioms", then no it's not possible, it would imply the axiom of choice

#### Mario Carneiro (Dec 05 2018 at 00:12):

However there is an interesting construction here for definite description with no axioms (well extensionality)

import data.set.basic

universes u
protected def set.definite_description {α : Type u}
{p : set α → Prop} (h : ∃! s, p s) : { s : set α // p s} :=
⟨{x : α | ∃ s, x ∈ s ∧ p s ∧ ∀ y, p y → y = s},
let ⟨s, ps, al⟩ := h in
have s = {x : α | ∃ s, x ∈ s ∧ p s ∧ ∀ y, p y → y = s},
from set.ext \$ λ x, ⟨λ xs, ⟨_, xs, ps, al⟩,
λ ⟨s', xs', ps', al'⟩, (al' _ ps).symm ▸ xs'⟩,
this ▸ ps⟩


#### Kenny Lau (Dec 05 2018 at 00:25):

@Mario Carneiro so... we can have a "computable" basis?

#### Mario Carneiro (Dec 05 2018 at 00:25):

"computable" but not computable

#### Mario Carneiro (Dec 05 2018 at 00:26):

when I revisited bases recently, we discussed changing the definition of a basis from a set to a family over a type. In that case it wouldn't be computationally irrelevant

Last updated: May 14 2021 at 04:22 UTC