## Stream: general

### Topic: prod.nonempty

#### Kevin Buzzard (Nov 17 2019 at 00:21):

What's the sensible proof of

example (X Y : Type) (hX : nonempty X) (hY : nonempty Y) : nonempty (X × Y) :=
begin
tactic.unfreeze_local_instances,
cases hX with x,
cases hY with y,
constructor,
exact x,y,
end

#### Mario Carneiro (Nov 17 2019 at 00:23):

example (X Y : Type) : nonempty X  nonempty Y  nonempty (X × Y)
| x y := (x, y)

#### Kevin Buzzard (Nov 17 2019 at 00:24):

Should this be an instance?

#### Mario Carneiro (Nov 17 2019 at 00:25):

yes, this looks like a good instance

#### Kevin Buzzard (Nov 17 2019 at 00:27):

Should this be a class:

class bounded_above (X : set ) : Prop :=
(is_bounded_above : bounded () X)

#### Kevin Buzzard (Nov 17 2019 at 00:28):

I'm trying to understand the fact that a non-empty bounded-above set has a unique least upper bound.

#### Kevin Buzzard (Nov 17 2019 at 00:29):

If $X$ and $Y$ are non-empty bounded-above sets of reals then so is $X+Y$. I'm wondering if typeclass inference has any business knowing this.

#### Mario Carneiro (Nov 17 2019 at 00:31):

it's debatable, but to me it seems like much ado about one theorem

#### Mario Carneiro (Nov 17 2019 at 00:32):

sometimes I wish we could just let theorems be theorems

#### Mario Carneiro (Nov 17 2019 at 00:33):

and just use them by name like normal people instead of going to incredible lengths to make everything appear wordless

#### Reid Barton (Nov 17 2019 at 01:22):

Names are annoying, but using type classes for theorems is worse

#### Kevin Buzzard (Nov 17 2019 at 02:08):

But the name of each of these theorems is NaN

#### Kevin Buzzard (Nov 17 2019 at 02:09):

I guess I do see your point.

Last updated: Dec 20 2023 at 11:08 UTC