Inf of Ioo in ℝ

Stream: new members

[Greg Price]

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]

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]

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]

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]

Mmm, that seems very plausible

[Mario Carneiro]

yep, real is not a complete_semilattice_Inf

[Mario Carneiro]

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

[Greg Price]

Huh, I see

[Greg Price]

Thanks!

[Eric Wieser]

docs#is_glb_Ioo for reference

[Greg Price]

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]

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]

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

[Greg Price]

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]

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]

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

[Greg Price]

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]

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]

Exactly

[Bhavik Mehta]

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