Sups and Infs for finite subsets of a lattice

Stream: Is there code for X?

[Paul Rowe]

Does Mathlib contain the fact that for a lattice, all nonempty finite sets have sups and infs?

import mathlib

lemma finSups {α : Type} [Lattice α] (F : Finset α) (ne : F.Nonempty) : ∃ a : α, IsLUB F a := sorry

lemma finInfs {α : Type} [Lattice α] (F : Finset α) (ne : F.Nonempty) : ∃ a : α, IsGLB F a := sorry

[Mitchell Lee]

There is docs#Finset.sup to get the sup, but no theorem that proves IsLUB for it

[Paul Rowe]

That seems to require OrderBot α which doesn't follow from Lattice α. (For example, the order dual of the naturals.)

For what it's worth, I have a proof of the above. But I wonder if there's value in making a PR for such a thing.

[Mitchell Lee]

I think that would have value for sure. Also, docs#Finset.sup' can be used to get the sup of a nonempty finset in a lattice without a bottom element.

[Paul Rowe]

Oh I missed the primed version. Good catch. I'll see if I can make it work with that choice because the approach I took was (needlessly) noncomputable.

[Paul Rowe]

It turns out the component pieces to prove the sup and inf are LUB and GLB respectively were already in Mathlib. The result is therefore the following.

import mathlib

lemma Finset.sup_isLUB {α : Type} [SemilatticeSup α] [OrderBot α] (F : Finset α) :
    IsLUB F (sup F id) := ⟨λ x h => id_eq x ▸ le_sup h, λ _ h => Finset.sup_le h⟩

lemma Finset.sup'_isLUB {α : Type} [SemilatticeSup α] {F : Finset α} (ne : F.Nonempty) :
    IsLUB F (sup' F ne id) := ⟨λ x h => id_eq x ▸ le_sup' id h, λ _ h => Finset.sup'_le ne id h⟩

lemma Finset.inf_isGLB {α : Type} [SemilatticeInf α] [OrderTop α] (F : Finset α) :
    IsGLB F (inf F id) := ⟨λ x h => id_eq x ▸ inf_le h, λ _ h => Finset.le_inf h⟩

lemma Finset.inf'_isGLB {α : Type} [SemilatticeInf α] {F : Finset α} (ne : F.Nonempty) :
    IsGLB F (inf' F ne id) := ⟨λ x h => id_eq x ▸ inf'_le id h, λ _ h => Finset.le_inf' ne id h⟩

If people think it's a good idea, I will open a PR with these additions when I find the time. (I'm stepping away from the computer for the rest of today.)

[Yaël Dillies]

Yeah sure looks reasonable!

[Yaël Dillies]

(please put isGLB before sup' in the name though)

[Paul Rowe]

PR #19961