# Zulip Chat Archive

## Stream: maths

### Topic: from le to ge by duality?

#### Jalex Stark (May 07 2020 at 17:44):

I have a theorem about `min`

s for an arbitrary linear order $M$. I'd like to get the dual theorems about `max`

by applying the first theorem to $M^{op}$ and then reinterpreting them in $M$. Is there any particular machinery to make this easier or should I just do it?

```
import tactic
import data.finset
import data.finsupp
import data.nat.basic
universes u
open_locale classical
open function
class DLO (α : Type u) extends decidable_linear_order α :=
(dense : ∀ a b : α, (a < b) → ∃ c, a < c ∧ c < b)
(without_top : ∀ a : α, ∃ b, a < b)
(without_bot : ∀ a : α, ∃ b, b < a)
variables {M N : Type u} [DLO M] [DLO N] [inhabited M] [inhabited N]
open pfun
example
-- given a finset in a DLO, produce an element below or above everything
def min_of_finset' (X : finset M) (X_nonempty : finset.nonempty X) : ∃ l ∈ X, ∀ x ∈ X, l ≤ x := finset.exists_min X id X_nonempty
def lb_of_finset (X : finset M) : ∃ l, ∀ x∈ X, l < x := begin
by_cases finset.nonempty X,
swap,
{ use arbitrary M,
intro x, intro hx,
unfold finset.nonempty at h, push_neg at h,
exfalso, exact h x hx},
-- maybe using have and contradiction is mathier in the above
have m := min_of_finset' _ h,
cases m with m hm,
cases hm with m_in_X hm,
have key := DLO.without_bot m,
cases key with l hl,
use l,
intros x hx,
apply lt_of_lt_of_le hl,
apply hm, assumption,
end
```

#### Jalex Stark (May 07 2020 at 17:46):

Hmm I guess the answer is going to be that the machinery is in the `category_theory`

library, so maybe I'll just do it "by hand" for now

#### Chris Hughes (May 07 2020 at 17:47):

You can use `order_dual`

#### Chris Hughes (May 07 2020 at 17:50):

The proof of the dual of lb_of_finset should be `@lb_of_finset (order_dual M) _ _`

. You have to put the right `DLO`

instance on `order_dual M`

for this to work. Put an instance for the recerse order on it.

#### Chris Hughes (May 07 2020 at 17:50):

There should already be a `linear_order`

instance.

#### Jalex Stark (May 07 2020 at 17:52):

hmm I don't know how to break up `DLO`

so that I can give the `linear_order`

and `without_*`

instance separately

#### Jalex Stark (May 07 2020 at 17:53):

In other words, I don't understand what the constructor is for typeclass that's made via `extends`

so probably I can answer this by reading TPiL

#### Yury G. Kudryashov (May 07 2020 at 17:59):

BTW, we already have `class no_top_order`

#### Yury G. Kudryashov (May 07 2020 at 18:00):

Moreover, we have classes `no_top_order`

, `no_bot_order`

and `densely_ordered`

#### Yury G. Kudryashov (May 07 2020 at 18:01):

So if you're writing for `mathlib`

, then you can use `[linear_order α] [no_bot_order α] [densely_ordered α]`

#### Yury G. Kudryashov (May 07 2020 at 18:02):

See also `directed.finset_le`

and `finset.exists_le`

in `algebra/big_operators`

.

#### Yury G. Kudryashov (May 07 2020 at 18:03):

So, for `finset.exists_lt`

you just need `[nonempty α] [directed_order α] [no_bot_order α]`

#### Yury G. Kudryashov (May 07 2020 at 18:04):

Note that we don't have a dual to `directed_order`

#### Yury G. Kudryashov (May 07 2020 at 18:05):

And we don't have any good instance for `directed_order`

. You can easily add `semilattice_inf.directed_order`

.

#### Jalex Stark (May 07 2020 at 18:22):

is there a way to bundle `linear_order`

, `no_top_order`

, ` no_bot_order`

and `densely_ordered`

into one class?

#### Jalex Stark (May 07 2020 at 18:24):

I can do this but then I'm carrying around new names? I really want to chain the extends

```
class DLO' (α : Type u) extends decidable_linear_order α :=
(dense : densely_ordered α)
(without_top : no_top_order α )
(without_bot : no_bot_order α )
```

#### David Wärn (May 07 2020 at 19:42):

I had this issue a while ago (working on the same kata!) (link). Mario recommended the solution you describe. My understanding is that chaining all the extends is problematic because `densely_ordered`

is parametrised by the order. You could at least combine `no_top_order`

, `no_bot_order`

and `densely_ordered`

into one class?

In the end I decided against defining a new class, and just did the back-and-forth argument with assumptions `decidable_linear_order`

, `no_top_order`

, ... for both types.

#### David Wärn (May 07 2020 at 19:43):

Btw, I think you might want `finset.max'`

/ `finset.min'`

?

Last updated: May 14 2021 at 18:28 UTC