The minimum of a `Set` if it exists else `bot`

Stream: Is there code for X?

[Ayhon]

In particular, I'm searching for a function of signature Set.min: (s: Set α) → s ≠ ∅ → WithBot α, defined as bot if the set is unbounded. Looking around I haven't managed to find it, but in case it is not defined elsewhere I would be interested in knowing how to best define it with the available definitions.

I was thinking something along the lines of

noncomputable
def Set.min{α: Type}[PartialOrder α](s: Set α)(s_nonempty: s ≠ ∅): WithBot α :=
  if h: ∃ (a: α), a = ⨅ s then
    a
  else
    ⊥

However, here I'm unable to picka out of the existential h (maybe with some Classical lemma?), and the BigOp ⨅ doesn't seem to be defined.

[Ayhon]

Closest I've gotten so far (playground):

import Mathlib

noncomputable
def Set.min{α: Type}[PartialOrder α](s: Set α)(h: s ≠ ∅): WithBot α :=
  let lbs: Type :=  {x : α // ∀ z ∈ s, x ≤ z}
  let mins : Type := {x : lbs // IsMin x}
  have : Decidable (Nonempty mins) := Classical.propDecidable _
  if h: Nonempty mins then
    let x := Classical.choice h
    x.val.val
  else
    ⊥

[Wrenna Robson]

So this is a thing that it is natural to want but is difficult for the reasons you have noted.

[Ayhon]

Actually, I've found a way of picking out of the existential with Classical.choose. This is what I have so far

open Classical in
noncomputable
def Set.min{α: Type}[PartialOrder α](s: Set α)(h: s ≠ ∅): WithBot α :=
  if h: ∃ x, (∀ z ∈ s, x ≤ z) ∧ (∀ x', (∀ z ∈ s, x' ≤ z) → x' ≤ x ) then
    (Classical.choose h: α)
  else
    ⊥

I'm just lacking some way of stating that x is a minimum a bit more nicely.

[Ayhon]

And I think that might be IsLeast :thinking:

[Wrenna Robson]

I think so

[Ayhon]

Ok, this is my current best. I opted to go for IsLUB in the end

import Mathlib

open Classical in
noncomputable
def Set.min{α: Type}[PartialOrder α](s: Set α)(_: s ≠ ∅): WithBot α :=
  if h : ∃ (x: α), IsLUB s x then
    (Classical.choose h: α)
  else
    ⊥

[Wrenna Robson]

That is not right.

[Wrenna Robson]

IsLUB doesn't make it a minimum

[Ayhon]

Oh, silly me

[Ayhon]

IsGLB

[Wrenna Robson]

No, the same

[Wrenna Robson]

IsLeast was correct

[Wrenna Robson]

IsLeast.csInf_eq

[Wrenna Robson]

See this

[Wrenna Robson]

which says that in a conditionally complete lattice, least elements are infimums

[Wrenna Robson]

IsLeast.csInf_mem

[Ayhon]

Hmmm

[Wrenna Robson]

And that the infimum is in the set

[Wrenna Robson]

Basically a minimum is an infimum which is in the set.

[Wrenna Robson]

BUT I do not think "bot" is a good choice for the default

[Wrenna Robson]

really what you want to do is either work in a (conditionally) complete lattice, OR embed into the lattice completion

[Wrenna Robson]

@Violeta Hernández Sorry to bother you - how do we spell the lattice completion again? We use Concept, right?

[Ayhon]

Maybe the issue is with the name then. I only need this to work with integers, picking the least element in the set or -\infty if its unbounded

[Wrenna Robson]

OK, that is much more reasonable as an ask :)

[Ayhon]

I wanted my definition to be general to hopefully make use of theorems in Mathlib, if present

[Ayhon]

But I'm just hoping to reason about intervals of extended integers WithTop (WithBot Int)

[Wrenna Robson]

Aye.

[Ayhon]

Why is my original ask problematic?

[Wrenna Robson]

I guess my advice is that it is somewhat unergonomic - it is not a good way to use existing mathlib stuff. I speak from experience!

[Violeta Hernández]

Wrenna Robson said:

Violeta Hernández Sorry to bother you - how do we spell the lattice completion again? We use Concept, right?

Yes, the Dedekind completion is the concept lattice of ≤. I have a sequence of PRs building up to that but the first one has been stuck for months because of some benchmarking shenanigans.

[Wrenna Robson]

Alas

[Ayhon]

I see

[Wrenna Robson]

Once we do have it, I do think a function that maps the inf/sup of a set into it would be good.

[Wrenna Robson]

Ayhon said:

I see

We do have ENat but we don't seem to have the extended integers.

[Wrenna Robson]

I assume there is a reason for this.

[Violeta Hernández]

Ayhon said:

But I'm just hoping to reason about intervals of extended integers WithTop (WithBot Int)

There's an open PR introducing the abbreviation EInt = WithBot (WithTop Int). I can find it once I'm on my computer.

[Ayhon]

There's actually a PR on its way

[Ayhon]

Yep, it was actually you, @Violeta Hernández, who mentioned it in a Zulip thread I posted a while back

[Ayhon]

There's also some added lemmas for WithTop (WithBot ·), if I remember correctly (up to correct ordering of WithTop/WithBot)

[Violeta Hernández]

I asked the PR author to move WithBotTop earlier so it could be used in the Order.WithBot file, but I think they've not yet done that

[Wrenna Robson]

Ah great.

[Violeta Hernández]

Yes, having a canonical spelling of "add both a bot and a top" is part of the reason I want this

[Wrenna Robson]

Yeah it makes sense

[Wrenna Robson]

you don't want to worry about the order

[Ayhon]

Violeta Hernández said:

I asked the PR author to move WithBotTop earlier so it could be used in the Order.WithBot file, but I think they've not yet done that

Are open PRs open to PRs?

[Violeta Hernández]

I think it's best to just ask the author directly. Or open a new PR with their permission.

[Ayhon]

I'll just leave a message letting them know I'd be willing to look into the final bit then

[Ayhon]

Actually, it seems like it's done, no? (#33876)

[Violeta Hernández]

I want WithBotTop to be available in the Order.WithBot file, but the PR currently defines it in a new file which then imports that one.

[Violeta Hernández]

I'll try this myself

[Violeta Hernández]

Of course I immediately run into problems

[Violeta Hernández]

I'll open a new thread about this

[Ayhon]

About the original question, I'm considering whether I should define my Set.min? as
sInf (WithBot.some '' s) by defining an instance of InfSet (WithBot α) whenever α has [LinearOrder α] [PredOrder α] [IsPredArchimedean α], so that I can apply BddBelow.exists_isLeast_of_nonempty on it. But this would basically mean defining InfSet.sInf to be what I already have, so I'm not sure it's worth it.

I just thought I'd share