iSup ≠ ⊤

Stream: Is there code for X?

[Snir Broshi]

import Mathlib
theorem foo {ι : Type*} {f : ι → ℕ∞} [Finite ι] (h : ∀ x, f x ≠ ⊤) : ⨆ x, f x ≠ ⊤ := by
  sorry

ENat is a CompleteLinearOrder so there's probably some lattice class that this statement works for, but I couldn't find a theorem for it.
As for proving it:
docs#iSup_eq_top seems almost helpful but not quite.
docs#ENat.iSup_coe_ne_top might help (applied to ENat.toNat ∘ f, plus docs#Finite.bddAbove_range) but I don't like that direction, especially since it's specific to ENat.

[Ruben Van de Velde]

import Mathlib
theorem foo {ι : Type*} {f : ι → ℕ∞} [Finite ι] (h : ∀ x, f x ≠ ⊤) : ⨆ x, f x ≠ ⊤ := by
  lift f to ι → ℕ using h
  simp only
  refine ENat.iSup_coe_ne_top.mpr ?_ -- apply?
  exact Finite.bddAbove_range f -- apply?

[Ruben Van de Velde]

But you found those

[Ruben Van de Velde]

Maybe this is a start

import Mathlib
theorem foo {ι : Type*} {f : ι → ℕ∞} [Finite ι] (h : ∀ x, f x ≠ ⊤) : ⨆ x, f x ≠ ⊤ := by
  lift f to ι → ℕ using h
  simp only [ne_eq]
  rw [iSup_eq_top, not_forall]
  have := Finite.bddAbove_range f
  rw [bddAbove_def] at this
  obtain ⟨b, hb⟩ := this
  use b
  simp_all

[Snir Broshi]

Cool, I didn't know about lift! But the lift is probably specific to ENat (or maybe to WithTop).
Do you know which lattice class this theorem holds for? Or maybe where I can find a Venn diagram of them?

[Kevin Buzzard]

It has nothing to do with Top. For any linear order it will be true that if f(x) isn't y for all x in some finite set then the sup of the f(x) won't be y, because the sup is just the max for a finite set in a linear order and in particular is attained.

[Snir Broshi]

Good point, although that also requires the set to be nonempty , or for iSup ∅ ≠ y
So it works for docs#CompleteLinearOrder (plus Nontrivial for ⊥ ≠ ⊤):

theorem foo {ι α : Type*} {f : ι → α} [Finite ι] [Nontrivial α] [CompleteLinearOrder α]
    (h : ∀ x, f x ≠ ⊤) : iSup f ≠ ⊤ := by
  cases isEmpty_or_nonempty ι
  · simp
  have ⟨x, hx⟩ := Set.range_nonempty f |>.csSup_mem <| Set.finite_range f
  exact (hx ▸ h x :)

Is it possible for a weaker class?

[Violeta Hernández]

As Kevin said, ⊤ is a red herring here. Replace it by any other value and the result will still be true (except potentially when ι is empty).

[Violeta Hernández]

Surely ConditionallyCompleteLinearOrder works as well?

[Snir Broshi]

Any other value y requires an iSup ∅ ≠ y hypothesis as I mentioned, unless I'm missing something

[Violeta Hernández]

Oh yeah, that is true. iSup Ø is pretty much just a non-specified junk value on anything other than an OrderTop.

[Aaron Liu]

this is why I like using IsGLB better than iSup or sSup or Finset.max' or Finset.sup or

[Violeta Hernández]

Someone really ought to unify all of these at some point

[Aaron Liu]

we have IsGLB

[Snir Broshi]

FWIW I added the theorem above as iSup_ne_top in #33501, used once in Finite.lean (search for Finite.lean, click "load diff", then search for iSup_ne_top), if you have any suggestions for it (ignoring the graph theory around it)

[Snir Broshi]

Basically it's used to show (f x).toNat ≤ (iSup f).toNat for g : α → Set α and f := Set.encard ∘ g given [Finite α]. It uses docs#ENat.toNat_le_toNat which requires ≠ ⊤

[Violeta Hernández]

Aaron Liu said:

we have IsGLB

I think there was a proposal at some point to turn sSup and sInf into functions defined on any partial order, such that sSup s = x if IsGLB s x, or sSup s = junk otherwise. The different conditionally/complete lattices would then have conditions on IsGLB/IsLUB, rather than on sSup/sInf.

[Violeta Hernández]

I don't remember the status of this. I think I was opposed to it since it would lead to bad def-eqs, but given that Set α and Unit are the only two types where there's any reasonable def-eq to begin with I now think that's actually completely acceptable.

[Violeta Hernández]

(On a related note, we could and probably should do the same for succ, defining succ x on any partial order as an arbitrary covering element, or x if none exists.)

[Violeta Hernández]

No wait, the actual proposal for sSup was to make a LawfulSup class with the IsGLB s (sSup s) assumption.

[Violeta Hernández]

#27534