# Zulip Chat Archive

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

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

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)$.

#### Heather Macbeth (Aug 29 2020 at 13:24):

Ah, nice!

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

Last updated: May 11 2021 at 16:22 UTC