complete lattice question

Stream: general

[Patrick Massot]

Is the following lemma true?

lemma infi_sup_right {α : Type*} {ι : Sort*} [complete_lattice α] (s : ι → α) (a : α) :
(⨅ i, s i) ⊔ a = ⨅ i, (s i ⊔ a) := sorry

It works for sets, but I'm worried this is not in the library. Of course I need it for filters :grinning:

[Kenny Lau]

the standard counter-example should be 0 < a,b,c < 1

[Kenny Lau]

and then you'd start requiring it be a complete_distrib_lattice, which solves the finite case, but I guess then there can be some infinite counter-example

[Patrick Massot]

Of course I meant complete_distrib_lattice

[Kenny Lau]

yeah and I'm saying there should be some analogous counter-example

[Kenny Lau]

emphasis on "should"

[Patrick Massot]

Wait, maybe complete_distrib_lattice is not what I thought.

[Kenny Lau]

can I do something like finite subsets of N and the full subset?

[Kenny Lau]

then have a = {0} and s n = {2n+1}

[Patrick Massot]

It seems the definition of complete_distrib_lattice is essentially that my lemma holds there.

[Kenny Lau]

oh really

[Kenny Lau]

class complete_distrib_lattice α extends complete_lattice α :=
(infi_sup_le_sup_Inf : ∀a s, (⨅ b ∈ s, a ⊔ b) ≤ a ⊔ Inf s)
(inf_Sup_le_supr_inf : ∀a s, a ⊓ Sup s ≤ (⨆ b ∈ s, a ⊓ b))

[Kenny Lau]

I see

[Patrick Massot]

Yes, it asks for inequalities only, but they are the problematic inequalities.

[Kenny Lau]

I wasn't even sure that complete_distrib_lattice exists when I said it

[Patrick Massot]

Ok, my new job is to prove filters on a given type form a completely distributive lattice. This works on paper (at least the inequality I need).

[Patrick Massot]

But I'm still very worried that Johannes didn't do it three years ago. This doesn't sound like something Johannes would have missed the opportunity to do.

[Reid Barton]

https://ncatlab.org/nlab/show/frame#definition

[Reid Barton]

and more information at https://ncatlab.org/nlab/show/distributive+lattice#infinitely_distributive_property

[Patrick Massot]

For the record: filters do not form a completely distributive lattice, because the other case (swapping sup and inf) does not hold. And the part that holds was already there, but through a little variation. My latest PR fills some of this little gap.