## Stream: maths

### Topic: complete_lattice (with_top ℕ)

#### Eric Wieser (Feb 12 2021 at 16:40):

Is this missing, or untrue?

#### Johan Commelin (Feb 12 2021 at 16:45):

I could only find

noncomputable instance : bounded_lattice enat :=
{ inf := min,
inf_le_left := min_le_left,
inf_le_right := min_le_right,
le_inf := λ _ _ _, le_min,
..enat.order_top,
..enat.semilattice_sup_bot }


#### Eric Wieser (Feb 12 2021 at 16:46):

Yeah, I can find a bounded_lattice on with_top nat too

#### Eric Wieser (Feb 12 2021 at 16:46):

My motivation was to apply docs#exists_mem_eq_sup, so I guess the assumptions on that lemma are too strict

#### Eric Wieser (Feb 12 2021 at 16:46):

And therfore a new bounded_linear_order typeclass is needed?
(class bounded_linear_order extends bounded_lattice β, linear_order β)

#### Rémy Degenne (Feb 12 2021 at 16:48):

You should get it from docs#with_top.complete_linear_order

@[instance]
def with_top.complete_linear_order {α : Type u_1} [conditionally_complete_linear_order_bot α] :
complete_linear_order (with_top α)


since we have that N is a conditionally_complete_linear_order_bot

#### Eric Wieser (Feb 12 2021 at 16:50):

Thanks, I needed to import order.conditionally_complete_lattice

#### Rémy Degenne (Feb 12 2021 at 16:53):

and there is also docs#enat.complete_linear_order

#### Eric Wieser (Feb 12 2021 at 16:57):

Bad things seem to happen when I use that instance:

import order.conditionally_complete_lattice
import data.finset.lattice

variables {ι : Type*} [fintype ι] (foo : ι → ℕ)

open finset

def min_or_zero : ℕ :=
option.get_or_else (univ.sup (λ v, foo v) : with_top ℕ) 0

lemma exists_eq_min_or_zero [nonempty ι] :
∃ v, foo v = min_or_zero foo :=
begin
obtain ⟨v', _, hv'⟩ :=
exists_mem_eq_sup finset.univ univ_nonempty (λ v, (foo v : with_top ℕ)),
refine ⟨v', _⟩,
unfold min_or_zero,
convert (option.get_or_else_coe _ _).symm,
convert hv',
sorry,
-- canonically_linear_ordered_add_monoid.semilattice_sup_bot = semilattice_sup_bot_of_bounded_lattice (with_top ℕ)
end


#### Eric Wieser (Feb 12 2021 at 16:58):

The enat version works, but roption.get_or_else is hard to use

#### Rémy Degenne (Feb 12 2021 at 16:59):

this is the same issue as the other day with ennreal, with canonically_linear_ordered_add_monoid causing duplicate sup/bot when using that instance of semilattice_sup_bot

#### Eric Wieser (Feb 12 2021 at 17:00):

The full state is

@canonically_linear_ordered_add_monoid.semilattice_sup_bot (with_top ℕ)
@semilattice_sup_bot_of_bounded_lattice (with_top ℕ)
(@complete_lattice.to_bounded_lattice (with_top ℕ)
(@complete_linear_order.to_complete_lattice (with_top ℕ)
(@with_top.complete_linear_order ℕ nat.conditionally_complete_linear_order_bot)))


#### Rémy Degenne (Feb 12 2021 at 17:03):

On branch#ennreal_lattice_issue I tried removing the instance canonically_linear_ordered_add_monoid.semilattice_sup_bot and after a small fix to one lemma about finsupp, it does not seem to cause any issue. But then you can't use any lemma for semilattice_sup_bot on a canonically_linear_ordered_add_monoid, which is a shame. I don't know enough about how those things work to be able to fix it

#### Rémy Degenne (Feb 12 2021 at 17:06):

The semilattice and order_bot parts of semilattice_sup_bot come from two different ancestors of canonically_linear_ordered_add_monoid. It looks like the way they are combined is not correct (in a way I don't understand)

#### Eric Wieser (Feb 12 2021 at 17:56):

This gives some hints of exactly what doesn't match - it's just the sup, the other operators are fine:

import order.conditionally_complete_lattice
import data.finset.lattice

variables {ι : Type*} [fintype ι] (foo : ι → ℕ)

open finset

def min_or_zero : ℕ :=
option.get_or_else (univ.sup (λ v, foo v) : with_top ℕ) 0

@[ext]
lemma semilattice_sup_bot.ext [α : Type*] (a b : semilattice_sup_bot α)
(h_bot : a.bot = b.bot) (h_sup : a.sup = b.sup) (h_le : a.le = b.le) (h_lt : a.lt = b.lt) : a = b :=
begin
casesI a, casesI b,
congr,
assumption',
end

lemma exists_eq_min_or_zero [nonempty ι] :
∃ v, foo v = min_or_zero foo :=
begin
obtain ⟨v', _, hv'⟩ :=
exists_mem_eq_sup finset.univ univ_nonempty (λ v, (foo v : with_top ℕ)),
refine ⟨v', _⟩,
unfold min_or_zero,
convert (option.get_or_else_coe _ _).symm,
convert hv',
ext1,
{ congr, },
{ dunfold semilattice_sup_bot.sup lattice.sup bounded_lattice.sup complete_lattice.sup
complete_linear_order.sup semilattice_sup_top.sup,
-- max = λ (o₁ o₂ : with_top ℕ), option.bind o₁ (λ (a : ℕ), option.map (λ (b : ℕ), a ⊔ b) o₂)
sorry },
{ congr, },
{ congr, },
end


Last updated: May 18 2021 at 06:15 UTC