# Zulip Chat Archive

## Stream: new members

### Topic: Inf of Ioo in ℝ

#### Greg Price (Apr 14 2021 at 06:51):

I'm trying to prove the fact that the infimum of a real interval $(a, b)$, with $a < b$, is the left endpoint $a$.

There are what seem to be the key pieces of this lying around -- but when I try to combine them, I get a puzzling type error:

```
import topology.instances.real
open set
lemma Inf_Ioo_R {a b : ℝ} (hab : a < b) : Inf (Ioo a b) = a := (is_glb_Ioo hab).Inf_eq
```

```
type mismatch at application
(is_glb_Ioo hab).Inf_eq
term
is_glb_Ioo hab
has type
is_glb (Ioo a b) a
but is expected to have type
is_glb ?m_3 ?m_4
```

#### Greg Price (Apr 14 2021 at 06:53):

I've learned that when I get an error that seems not to make sense in that particular way -- i.e. it seems like the actual and expected type perfectly well do match -- it's usually helpful to set `pp.implicit true`

, or even `pp.all true`

.

But in this case that's leaving me still puzzled:

#### Mario Carneiro (Apr 14 2021 at 06:54):

That kind of error usually means the theorem requires a typeclass that the target doesn't support. In this case I would guess that real is not a complete lattice

#### Greg Price (Apr 14 2021 at 06:54):

```
import topology.instances.real
open set
set_option pp.implicit true
lemma Inf_Ioo_R' {a b : ℝ} (hab : a < b) : Inf (Ioo a b) = a := (is_glb_Ioo hab).Inf_eq
```

```
type mismatch at application
(@is_glb_Ioo ℝ real.linear_order (@linear_ordered_field.to_densely_ordered ℝ real.linear_ordered_field) a b
hab).Inf_eq
term
@is_glb_Ioo ℝ real.linear_order (@linear_ordered_field.to_densely_ordered ℝ real.linear_ordered_field) a b hab
has type
@is_glb ℝ
(@partial_order.to_preorder ℝ
(@semilattice_inf.to_partial_order ℝ
(@lattice.to_semilattice_inf ℝ (@lattice_of_linear_order ℝ real.linear_order))))
(@Ioo ℝ
(@partial_order.to_preorder ℝ
(@semilattice_inf.to_partial_order ℝ
(@lattice.to_semilattice_inf ℝ (@lattice_of_linear_order ℝ real.linear_order))))
a
b)
a
but is expected to have type
@is_glb ?m_1 (@partial_order.to_preorder ?m_1 (@complete_semilattice_Inf.to_partial_order ?m_1 ?m_2)) ?m_3 ?m_4
```

#### Greg Price (Apr 14 2021 at 06:54):

Mmm, that seems very plausible

#### Mario Carneiro (Apr 14 2021 at 06:55):

yep, real is not a `complete_semilattice_Inf`

#### Mario Carneiro (Apr 14 2021 at 06:55):

You should try to find a variation on the theorem that works for conditionally complete lattices

#### Greg Price (Apr 14 2021 at 06:56):

Huh, I see

#### Greg Price (Apr 14 2021 at 06:57):

Thanks!

#### Eric Wieser (Apr 14 2021 at 07:00):

docs#is_glb_Ioo for reference

#### Greg Price (Apr 14 2021 at 07:00):

Yup, here's a working version:

```
lemma Inf_Ioo_R {a b : ℝ} (hab : a < b) : Inf (Ioo a b) = a :=
(is_glb_Ioo hab).cInf_eq (nonempty_Ioo.mpr hab)
```

#### Greg Price (Apr 14 2021 at 07:01):

Eric Wieser said:

docs#is_glb_Ioo for reference

This is one of the theorems I was using, right? Or was that your point :smile:

#### Eric Wieser (Apr 14 2021 at 07:02):

That was my point - but I can't see why that lemma wouldn't apply

#### Greg Price (Apr 14 2021 at 07:02):

That part was working fine, I think, but then it was the `Inf_eq`

that was failing, because it wanted a complete lattice

#### Greg Price (Apr 14 2021 at 07:03):

Which $\mathbb R$ isn't, but it is a "conditionally complete lattice" which is a term I'd never heard before but perfectly captures the relevant familiar property of $\mathbb R$

#### Greg Price (Apr 14 2021 at 07:03):

So docs#is_glb.cInf_eq is the right version of that lemma

#### Greg Price (Apr 14 2021 at 07:07):

And ftr here's the version of this little lemma in (what I believe is) the appropriate generality -- nothing changes except replacing $\mathbb R$ with some typeclasses:

```
variables {γ : Type*} [conditionally_complete_linear_order γ] [densely_ordered γ]
lemma Inf_Ioo {a b : γ} (hab : a < b) : Inf (Ioo a b) = a :=
(is_glb_Ioo hab).cInf_eq (nonempty_Ioo.mpr hab)
```

#### Kevin Buzzard (Apr 14 2021 at 08:08):

It almost feels like one doesn't need the conditionally complete assumption, if one has `densely_ordered`

. Is the issue that without conditionally complete there is no _definition_ of Inf?

#### Eric Wieser (Apr 14 2021 at 08:18):

Exactly

#### Bhavik Mehta (Apr 14 2021 at 13:17):

Could you make a PR for this? I found myself needing Inf_Ioi over the reals yesterday too

Last updated: May 09 2021 at 19:11 UTC