## Stream: maths

### Topic: Errors with order hierarchy

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

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

#### Mario Carneiro (Aug 29 2020 at 03:54):

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

#### Heather Macbeth (Aug 29 2020 at 03:57):

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

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

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

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

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

#### Mario Carneiro (Aug 29 2020 at 04:14):

Do by_cases h : nonempty A

Thanks!!

#### Mario Carneiro (Aug 29 2020 at 04:14):

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

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

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


#### Heather Macbeth (Aug 29 2020 at 04:33):

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

#### Sebastien Gouezel (Aug 29 2020 at 08:08):

It is not true for arbitrary nonempty open subsets of $\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.

#### Sebastien Gouezel (Aug 29 2020 at 08:09):

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

Ah, nice!

#### Heather Macbeth (Aug 31 2020 at 04:33):

#3991

Last updated: May 11 2021 at 16:22 UTC