# Zulip Chat Archive

## 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: Aug 03 2023 at 10:10 UTC