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