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

Stream: maths

[Ryan Lahfa]

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]

The theorem is false

[Mario Carneiro]

If the set fails to be bounded below, Inf returns garbage, and that garbage value may happen to lie in the set

[Ryan Lahfa]

Ah, so that's the problem

[Mario Carneiro]

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

[Ryan Lahfa]

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

[Mario Carneiro]

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

[Mario Carneiro]

is_glb

[Ryan Lahfa]

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

[Yury G. Kudryashov]

We want to write Sup s or Inf s before we prove that s has a lub/glb.

[Yury G. Kudryashov]

Once you have is_least, AFAIR we have is_least.bdd_below.

[Yury G. Kudryashov]

And I hope that we have is_least.cInf_eq (or is it is_least.is_glb.cInf_eq?)