# Zulip Chat Archive

## Stream: maths

### Topic: If some inf is a min, then the set is bounded below

#### Ryan Lahfa (Apr 03 2020 at 14:58):

I'm looking at this lemma:

import data.set import data.set.finite import data.finset import order.conditionally_complete_lattice variable {X: Type} open classical local attribute [instance] prop_decidable lemma inf_mem_then_set_bounded [conditionally_complete_linear_order X] (S: set X): Inf S ∈ S → bdd_below S := sorry

While playing around with the lattices API ; but I'm not sure how to prove the statement.

I cannot use Inf_ge because it requires bdd_below, so my only option is to say that an Inf which is in the set, is a Min, i.e. is_least S (Inf S) is true.

So I tried to go for this but it requires Inf S to be in lower_bounds, which appears to be true by def?

Even if I'm in a conditional complete lattice, I can always wrap it into a complete lattice by adding bottom and top to extend X.

Using this, I can take Inf of anything, including empty sets, etc. As I have Inf S in S, it fix my problem.

But I'm unsure how to proceed to promote X into a X' with complete_linear_order over it and bring my assumptions over there, finish my proof, come back to the X world.

#### Mario Carneiro (Apr 03 2020 at 15:00):

The theorem is false

#### Mario Carneiro (Apr 03 2020 at 15:00):

If the set fails to be bounded below, `Inf`

returns garbage, and that garbage value may happen to lie in the set

#### Ryan Lahfa (Apr 03 2020 at 15:00):

Ah, so that's the problem

#### Mario Carneiro (Apr 03 2020 at 15:01):

for example if the garbage value is 0, then `Inf (-inf, 0] \in (-inf, 0]`

#### Ryan Lahfa (Apr 03 2020 at 15:01):

But I don't understand why Inf does not use option-types, wouldn't it make more sense?

#### Mario Carneiro (Apr 03 2020 at 15:01):

That would amount to a predicate formulation, and that already exists without any conditionally complete anything

#### Mario Carneiro (Apr 03 2020 at 15:01):

`is_glb`

#### Ryan Lahfa (Apr 03 2020 at 15:02):

Okay, makes more sense then, I'll use this, thank you!

#### Yury G. Kudryashov (Apr 03 2020 at 23:30):

We want to write `Sup s`

or `Inf s`

before we prove that `s`

has a `lub`

/`glb`

.

#### Yury G. Kudryashov (Apr 03 2020 at 23:30):

Once you have `is_least`

, AFAIR we have `is_least.bdd_below`

.

#### Yury G. Kudryashov (Apr 03 2020 at 23:31):

And I hope that we have `is_least.cInf_eq`

(or is it `is_least.is_glb.cInf_eq`

?)

Last updated: May 06 2021 at 18:20 UTC