Zulip Chat Archive

Stream: new members

Topic: Inf of Ioo in ℝ


view this post on Zulip Greg Price (Apr 14 2021 at 06:51):

I'm trying to prove the fact that the infimum of a real interval (a,b) (a, b) , with a<b a < b , is the left endpoint a 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

view this post on Zulip 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:

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Greg Price (Apr 14 2021 at 06:54):

Mmm, that seems very plausible

view this post on Zulip Mario Carneiro (Apr 14 2021 at 06:55):

yep, real is not a complete_semilattice_Inf

view this post on Zulip Mario Carneiro (Apr 14 2021 at 06:55):

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

view this post on Zulip Greg Price (Apr 14 2021 at 06:56):

Huh, I see

view this post on Zulip Greg Price (Apr 14 2021 at 06:57):

Thanks!

view this post on Zulip Eric Wieser (Apr 14 2021 at 07:00):

docs#is_glb_Ioo for reference

view this post on Zulip 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)

view this post on Zulip 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:

view this post on Zulip Eric Wieser (Apr 14 2021 at 07:02):

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

view this post on Zulip 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

view this post on Zulip Greg Price (Apr 14 2021 at 07:03):

Which R \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 R \mathbb R

view this post on Zulip Greg Price (Apr 14 2021 at 07:03):

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

view this post on Zulip 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 R \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)

view this post on Zulip 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?

view this post on Zulip Eric Wieser (Apr 14 2021 at 08:18):

Exactly

view this post on Zulip 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