## Stream: maths

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

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

I have a theorem about mins 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