# Zulip Chat Archive

## 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