Zulip Chat Archive

Stream: maths

Topic: Errors with order hierarchy


view this post on Zulip Heather Macbeth (Aug 28 2020 at 21:17):

I contributed some theorems for conditionally complete linear orders (#3843), now I want to use them for real analysis. How can I get the conditionally complete linear order property for an interval? I want:

variables [conditionally_complete_linear_order α] {a b : α}

instance subtype.conditionally_complete_linear_order :
  conditionally_complete_linear_order (Ioo a b) :=
sorry

Since mathlib already has docs#subtype.linear_order, I had thought it might be enough to show the 4 new properties for docs#conditionally_complete_linear_order, doing something like

instance subtype.conditionally_complete_linear_order :
  conditionally_complete_linear_order (Ioo a b) :=
{ le_cSup := _,
  cSup_le := _,
  cInf_le := _,
  le_cInf := _,
  ..subtype.linear_order (Ioo a b) }

But this gives me no end of errors -- things like, "invalid structure value { ... }, field 'sup' was not provided".

view this post on Zulip Heather Macbeth (Aug 29 2020 at 03:52):

With some trial and error, I got this working as

noncomputable instance subtype.conditionally_complete_lattice [inhabited (Ioo a b)] :
  conditionally_complete_lattice (Ioo a b) :=
{ Sup := _,
  le_cSup := _,
  cSup_le := _,
  Inf := _,
  cInf_le := _,
  le_cInf := _,
  ..distrib_lattice.to_lattice (Ioo a b) }

for suitable _.

view this post on Zulip Mario Carneiro (Aug 29 2020 at 03:54):

You know, I think this is true for any open subset of R

view this post on Zulip Heather Macbeth (Aug 29 2020 at 03:57):

You mean, without the inhabited? Yes, I am playing with that at the moment.

view this post on Zulip Heather Macbeth (Aug 29 2020 at 03:59):

I use the inhabited in order to define

Sup := λ t, if ht : Sup (coe '' t : set α)  (Ioo a b) then Sup (coe '' t : set α), ht else default (Ioo a b),

Hard to avoid this, but I could do a case analysis with a separate case for non-inhabited α. Is there a typeclass for empty α or similar? I haven't had to reason about them before.

view this post on Zulip Heather Macbeth (Aug 29 2020 at 04:05):

Oh -- maybe you mean any open subset, not just an interval. That may well be true, but I think it fits less well in the library. The statement about open intervals can live in order.conditionally_complete_lattice. The statement about open sets would have to be deferred to topology.algebra.ordered.

view this post on Zulip Mario Carneiro (Aug 29 2020 at 04:11):

I don't mean the instance should be registered, just that it is a mathematically more general theorem

view this post on Zulip Heather Macbeth (Aug 29 2020 at 04:13):

While I have your attention ( :smiley:), how do I do this?

Heather Macbeth said:

I could do a case analysis with a separate case for non-inhabited α. Is there a typeclass for empty α or similar? I haven't had to reason about them before.

view this post on Zulip Mario Carneiro (Aug 29 2020 at 04:14):

Do by_cases h : nonempty A

view this post on Zulip Heather Macbeth (Aug 29 2020 at 04:14):

Thanks!!

view this post on Zulip Mario Carneiro (Aug 29 2020 at 04:14):

under the assumption that it is false, you can prove that A is empty

view this post on Zulip Mario Carneiro (Aug 29 2020 at 04:15):

we don't have any particular typeclass for this but generally whatever you are proving will become trivial under this assumption

view this post on Zulip Heather Macbeth (Aug 29 2020 at 04:17):

Do I need to enter tactic mode in my definition, then? Is there a more idiomatic way?

noncomputable instance subtype.conditionally_complete_linear_order :
  conditionally_complete_linear_order (Ioo a b) :=
begin
  by_cases h : nonempty (Ioo a b),
  { sorry },
  { sorry }
end

view this post on Zulip Heather Macbeth (Aug 29 2020 at 04:33):

Never mind -- the inhabited hypothesis is necessary. docs#has_Sup_to_nonempty

view this post on Zulip Sebastien Gouezel (Aug 29 2020 at 08:08):

It is not true for arbitrary nonempty open subsets of R\mathbb{R}. Consider for instance the union A of the open intervals centered at 1/n of small enough radius r_n to make sure that these intervals are disjoint, and of (-1, 0). Then the intersection of A with the positive half-line has no Inf in A, even though it is bounded below.

view this post on Zulip Sebastien Gouezel (Aug 29 2020 at 08:09):

Better example: (1,0)(0,1)(-1, 0) \cup (0,1).

view this post on Zulip Heather Macbeth (Aug 29 2020 at 13:24):

Ah, nice!

view this post on Zulip Heather Macbeth (Aug 31 2020 at 04:33):

#3991


Last updated: May 11 2021 at 16:22 UTC