# Zulip Chat Archive

## 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 ℕ)
(@with_top.canonically_linear_ordered_add_monoid ℕ nat.canonically_linear_ordered_add_monoid) =
@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