Zulip Chat Archive

Stream: maths

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


view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Apr 03 2020 at 15:00):

The theorem is false

view this post on Zulip 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

view this post on Zulip Ryan Lahfa (Apr 03 2020 at 15:00):

Ah, so that's the problem

view this post on Zulip Mario Carneiro (Apr 03 2020 at 15:01):

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

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Apr 03 2020 at 15:01):

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

view this post on Zulip Mario Carneiro (Apr 03 2020 at 15:01):

is_glb

view this post on Zulip Ryan Lahfa (Apr 03 2020 at 15:02):

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

view this post on Zulip 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.

view this post on Zulip Yury G. Kudryashov (Apr 03 2020 at 23:30):

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

view this post on Zulip 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