# Zulip Chat Archive

## Stream: Is there code for X?

### Topic: finset.sup'

#### Scott Morrison (Apr 12 2021 at 05:39):

No one has `finset.sup'`

(for nonempty finsets, but only requiring `semilattice_sup`

rather than `semilattice_sup_bot`

) up their sleeves, do they? It seems like an obvious omission, but I'm not so keen to go fill it in right now. :-)

#### Eric Wieser (Apr 12 2021 at 05:43):

There's a recent open PR for this

#### Scott Morrison (Apr 12 2021 at 05:44):

I better go review it! :-)

#### Scott Morrison (Apr 12 2021 at 05:45):

#### Scott Morrison (Apr 12 2021 at 05:49):

It already looks in great shape. (Thanks, @Alistair Tucker, for having exactly what I wanted ready. :-)

#### Scott Morrison (Apr 12 2021 at 05:51):

#### Eric Wieser (Apr 12 2021 at 06:11):

That PR raises an omission in our naming guide, with `finset.of_sup_of_forall`

- how should lemmas be named when their conclusion is `p (f x)`

, where `p`

is an argument passed to the lemma?

#### Mario Carneiro (Apr 12 2021 at 06:39):

That theorem actually looks like an induction principle. I would call it `sup_induction`

or something like that

#### Scott Morrison (Apr 12 2021 at 09:08):

@Alistair Tucker, I'm finding I need

```
@[simp] lemma lt_sup'_iff [is_total α (≤)] (a : α) : a < s.sup' H f ↔ (∃ b ∈ s, a < f b) :=
```

Any chance you want to do the `le`

version, and the `inf'`

analogues?

#### Scott Morrison (Apr 12 2021 at 09:09):

I have a terrible proof of the above...

#### Ruben Van de Velde (Apr 12 2021 at 09:45):

How do you feel about this?

```
import data.finset
variables {α β : Type*} [semilattice_sup α]
open finset
lemma sup_of_mem {s : finset β} (f : β → α) {b : β} (h : b ∈ s) :
∃ (a : α), s.sup (coe ∘ f : β → with_bot α) = ↑a := sorry
def finset.sup' (s : finset β) (H : s.nonempty) (f : β → α) : α :=
option.get $ let ⟨b, hb⟩ := H in option.is_some_iff_exists.2 (sup_of_mem f hb)
variables {s : finset β} (H : s.nonempty) (f : β → α)
lemma sup'_le {a : α} (hs : ∀ b ∈ s, f b ≤ a) : s.sup' H f ≤ a := sorry
@[simp] lemma sup'_le_iff {a : α} : s.sup' H f ≤ a ↔ ∀ b ∈ s, f b ≤ a := sorry
@[simp] lemma not_lt' [is_total α (≤)] {a b : α} : ¬ a < b ↔ b ≤ a :=
begin
split; intro h,
{ cases total_of (≤) a b with h1 h1,
{ rw h1.lt_or_eq.resolve_left h },
{ exact h1 } },
{ cases total_of (≤) a b with h1 h1,
{ rw le_antisymm h h1, apply lt_irrefl },
{ exact not_lt_of_le h } },
end
@[simp] lemma lt_sup'_iff [is_total α (≤)] (a : α) (s : finset β) (H : s.nonempty) (f : β → α) :
a < s.sup' H f ↔ (∃ b ∈ s, a < f b) :=
begin
suffices : ¬(a < s.sup' H f) ↔ ¬(∃ b ∈ s, a < f b),
{ have := not_congr this,
rwa [not_not, not_not] at this },
push_neg,
simp_rw [not_lt', sup'_le_iff H f]
end
```

#### Eric Wieser (Apr 12 2021 at 09:50):

Why doesn't docs#not_lt work for you there? Do we have examples where `[is_total α (≤)]`

but not `[linear_order α]`

?

#### Eric Wieser (Apr 12 2021 at 09:58):

`not_lt'`

golfs slightly to:

```
@[simp] lemma not_lt' [semilattice_sup α] [is_total α (≤)] {a b : α} : ¬ a < b ↔ b ≤ a :=
@not_lt _ {
le_total := is_total.total,
decidable_le := classical.dec_rel _,
decidable_eq := classical.dec_eq _,
decidable_lt := classical.dec_rel _,
..(infer_instance : partial_order α) } _ _
```

#### Eric Wieser (Apr 12 2021 at 09:59):

But this feels silly, because

```
example {α} [linear_order α] : semilattice_sup α := infer_instance
```

#### Eric Wieser (Apr 12 2021 at 10:00):

So I think `is_total`

is probably a wrong turn in @Scott Morrison's requested statement

#### Ruben Van de Velde (Apr 12 2021 at 10:17):

It's nicer with `linear_order`

, definitely.

```
@[simp] lemma lt_sup'_iff [linear_order α] (a : α) (s : finset β) (H : s.nonempty) (f : β → α) :
a < s.sup' H f ↔ (∃ b ∈ s, a < f b) :=
begin
split; { contrapose!, rw sup'_le_iff H f, exact id }
end
```

Even better if `contrapose`

handled iffs

#### Scott Morrison (Apr 12 2021 at 11:17):

Thanks @Ruben Van de Velde, that's nice! I can roll this, and the variations, into an upcoming PR, unless you feel like getting to them first!

#### Ruben Van de Velde (Apr 12 2021 at 11:21):

No, go for it

#### Bhavik Mehta (Apr 12 2021 at 11:36):

Eric Wieser said:

Why doesn't docs#not_lt work for you there? Do we have examples where

`[is_total α (≤)]`

but not`[linear_order α]`

?

I don't know if we have examples in mathlib yet but it's not hard to come up with examples in maths - Peter mentioned one a couple of days ago: consider the order given by `inv_image`

where the target is a linear order, then the new order is a total preorder but it's not antisymmetric

#### Eric Wieser (Apr 12 2021 at 12:37):

In the example above there was already a `[semilattice_sup α]`

assumption - but I see I didn't make it clear in that question

#### Alistair Tucker (Apr 12 2021 at 15:12):

Following the pattern in the rest of the file, one would first prove that

```
lemma lt_sup_iff [is_total α (≤)] {a : α} : a < s.sup f ↔ (∃ b ∈ s, a < f b)
```

(It should be in there anyway for completeness.) Then it's pretty straightforward to do a version for `sup'`

.

```
lemma lt_sup'_iff [is_total α (≤)] {a : α} : a < s.sup' H f ↔ (∃ b ∈ s, a < f b) :=
begin
rw [←with_bot.coe_lt_coe, coe_sup', lt_sup_iff],
exact bex_congr (λ b hb, with_bot.coe_lt_coe),
end
```

#### Alistair Tucker (Apr 12 2021 at 15:13):

There was some reason why I had to go down the `is_total`

route rather than `linear_order`

but I can't remember right now

#### Alistair Tucker (Apr 12 2021 at 15:21):

I would probably have proved `lt_sup_iff`

by induction like so

```
lemma lt_sup_iff [is_total α (≤)] {a : α} : a < s.sup f ↔ ∃ b ∈ s, a < f b :=
begin
split,
{ intro h,
induction s using finset.cons_induction with b s hb ih,
{ exact false.elim (not_lt_bot h), },
{ rw [sup_cons, _root_.lt_sup_iff] at h,
cases h,
{ exact ⟨b, mem_cons.2 (or.inl rfl), h⟩, },
{ rcases ih h with ⟨c, hc, hlt⟩,
exact ⟨c, mem_cons.2 (or.inr hc), hlt⟩, }, }, },
{ rintro ⟨b, hb, hlt⟩,
exact lt_of_lt_of_le hlt (le_sup hb), },
end
```

But maybe Ruben's proof points to a better way... let me check.

#### Eric Wieser (Apr 12 2021 at 16:23):

You probably went down the `is_total`

route because `[linear_order α] [semilattice_sup α]`

introduced two different `has_le`

s

#### Eric Wieser (Apr 12 2021 at 16:25):

But `[linear_order α]`

by itself induces a `semilattice_sup α`

anyway, so there's no need for both

#### Alistair Tucker (Apr 12 2021 at 16:53):

I've made a branch for this. Based on Ruben's proof although it turns out there is such a thing as `as_linear_order`

which makes it considerably shorter. @Ruben Van de Velde or @Eric Wieser would either of you like to make changes and/or a PR? I suppose Scott will be asleep atm.

#### Alistair Tucker (Apr 12 2021 at 16:54):

Oops https://github.com/leanprover-community/mathlib/tree/lt_sup_iff

#### Alistair Tucker (Apr 12 2021 at 16:56):

You probably went down the

`is_total route`

because...

Maybe something about having `bot`

? I'll check later

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

I'd missed that your last PR already added the `is_total`

arguments - I'll play with removing them

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

Do we have those arguments on lemmas about docs#finset.max'?

#### Eric Wieser (Apr 12 2021 at 17:04):

Oh you're right, `bot`

is indeed the issue

#### Eric Wieser (Apr 12 2021 at 17:05):

Which was needed for `sup`

, but not `sup'`

#### Eric Wieser (Apr 12 2021 at 17:11):

But `sup`

is still a mess for similar reasons. Perhaps we should have a `linear_order_bot`

and `linear_order_top`

class, to sit between docs#linear_order and docs#complete_linear_order?

#### Kevin Buzzard (Apr 12 2021 at 18:36):

When I was a lad back in 2017, there was just lattice, semilattice_sup_bot, semilattice_inf_top, conditionally_complete_lattice, and then complete_lattice. Then people wanted semilattice_sup_top and semilattice_inf_bot, and now we're getting variants with total orders. Similarly we now seem to have monoids with 0, add_monoids with 1 and so on. My impression is that given any subset of the set of all notation coming up in the topological hierarchy, sooner or later someone will want an object which has all of the subset but nothing else, because their favourite mathematical object has precisely this subset but not the rest. The same is happening in the algebraic heirarchy -- all this distrib_mul_action stuff is what you get with + and * but no 0 or 1, for example, with added heterogeneous issues thrown in. People seem really reluctant to pull off everything into pieces, because then complete_lattice would extend has_bot, has_top, has_sup, has_Sup, has_inf, has_Inf and then there would be a gazillion Props on top. But my impression is that this is somehow the way we're moving. Is there some more principled way of doing this stuff rather than just inventing 2^N new typeclasses?

#### Eric Wieser (Apr 12 2021 at 20:45):

I believe that the defs in core around src#is_total was an attempt at such a principled approach - there seems to be an `@[algebra]`

attribute for some feature that I can only assume never materialized.

#### Alistair Tucker (Apr 13 2021 at 07:19):

@Eric Wieser So should we regard `is_total`

as a great thing or as an outdated piece of junk? You don't seem to approve of it but for example a version of `exists_mem_eq_sup`

written for `[semilattice_sup_bot α] [is_total α (≤)]`

instead of `[complete_linear_order α ]`

would resolve the problem with `ℕ`

that cropped up in this thread https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/strict.20instance.20requirement.

#### Eric Wieser (Apr 13 2021 at 07:21):

I'm no longer sure

#### Mario Carneiro (Apr 13 2021 at 07:23):

It's useful when working with general relations that aren't the le on the type

#### Eric Wieser (Apr 13 2021 at 07:23):

If `is_total (\le)`

is a good thing, then we should change as many lemmas as possible to use it instead of linear_order

#### Mario Carneiro (Apr 13 2021 at 07:24):

A total semilattice is a lattice

#### Mario Carneiro (Apr 13 2021 at 07:24):

in fact it is a linear order

#### Mario Carneiro (Apr 13 2021 at 07:25):

Maybe we need `linear_order_bot`

?

#### Eric Wieser (Apr 13 2021 at 07:26):

Either we need that, or we need to switch to using is_total as a mixing for totality

#### Mario Carneiro (Apr 13 2021 at 07:26):

how many theorems need this combo?

#### Eric Wieser (Apr 13 2021 at 07:27):

Currently we're in a middle ground where we have to switch between the two and end up reproving things like `not_lt_iff`

as happened up thread

#### Eric Wieser (Apr 13 2021 at 07:27):

I think I found 2 within finset.lattice, and another two for the top version

#### Mario Carneiro (Apr 13 2021 at 07:27):

if it's only those then I guess the `is_total`

mixin is fine

#### Eric Wieser (Apr 13 2021 at 07:28):

I haven't searched mathlib-wide

#### Mario Carneiro (Apr 13 2021 at 07:28):

That's okay, you can just convert lemmas when you find them / need them

#### Mario Carneiro (Apr 13 2021 at 07:29):

Looking `is_total`

up is more expensive since it's two typeclass searches with one dependent on the other, so I don't think we want to use too many mixins

#### Eric Wieser (Apr 13 2021 at 07:44):

Doesn't the dependency make it less expensive?

Last updated: May 17 2021 at 16:26 UTC