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