# Zulip Chat Archive

## Stream: new members

### Topic: opposite preorder

#### Iocta (Aug 03 2020 at 00:59):

I am learning about preorders, and I read there is a concept called "opposite preorder", which is, Given a preorder (P, <=), the opposite is a preorder (P, <=op) having p <=op q iff q <= p. I am wondering how to write this in lean. I found preorders in lean. Is that definition suitable for defining 'opposite preorder' with? How to do that?

#### Reid Barton (Aug 03 2020 at 01:02):

it's called docs#order_dual in mathlib

#### Adam Topaz (Aug 03 2020 at 01:13):

Oooh should this be a job for docs#opposite ?

#### Reid Barton (Aug 03 2020 at 01:15):

`opposite`

is already sort of conceptually dubious but it definitely shouldn't reverse both `<=`

and `*`

#### Adam Topaz (Aug 03 2020 at 01:15):

Oh yeah fair enough. Didn't consider the case of an ordered ring.

#### Adam Topaz (Aug 03 2020 at 01:18):

Well... If you think of a poset as a category, then opposite does make sense.

#### Yury G. Kudryashov (Aug 03 2020 at 03:23):

Possibly we should split `opposite`

in category theory and in group theory and turn `ᵒᵖ`

into two `localized notation`

s.

#### Iocta (Aug 03 2020 at 18:08):

A couple questions

```
import data.set.basic
import data.set.lattice
import data.setoid.partition
import order.filter.basic
import tactic.basic
import tactic
import init.logic init.classical init.meta.name init.algebra.classes
variable X : Type
variable s : set X
variable {P : set X}
-- XXX Don't I mean [preorder P], not [preorder X]?
def is_upper [preorder X] (P: set X) : Prop :=
∀ p ∈ P, ∀ (q : X), q ≥ p → q ∈ P
def uparrow [preorder X] (p : X) (hp: p ∈ P) : set X :=
{p' ∈ P | p ≤ p'}
-- XXX Why doesn't this work?
example [preorder X] (p : X) : ∀ p ∈ P, is_upper (uparrow p) := sorry
```

```
failed to synthesize type class instance for
X : Type,
P : set X,
_inst_1 : preorder X,
p : X,
p : Type
⊢ has_mem Type (set X)
cats.lean:23:50
failed to synthesize type class instance for
X : Type,
P : set X,
_inst_1 : preorder X,
p : X,
p : Type,
H : p ∈ P
⊢ preorder p
```

#### Reid Barton (Aug 03 2020 at 18:16):

Check the type of `uparrow`

. It has more explicit arguments than you seem to think

#### Jalex Stark (Aug 03 2020 at 18:19):

it might help you to squash your three `variable`

statements into one `variables`

statement

#### Iocta (Aug 03 2020 at 18:29):

```
uparrow : Π (X : Type) {P : set X} [_inst_1 : preorder X] (p : X), p ∈ P → set X
```

has two of `(these)`

so I think it needs two arguments

but

```
example [preorder X] (p : X) : ∀ p ∈ P, is_upper (uparrow X p) := sorry
type mismatch at application
is_upper (uparrow X p)
term
uparrow X p
has type
p ∈ ?m_1 → set X : Type
but is expected to have type
Type : Type 1
```

#### Jalex Stark (Aug 03 2020 at 18:30):

do you know what the type of `uparrow X p`

is?

#### Iocta (Aug 03 2020 at 18:31):

```
p ∈ ?m_1 → set X : Type
```

apparently

#### Iocta (Aug 03 2020 at 18:34):

does that mean I'm supposed to change it from forall to introducing a specific `hp : p \in P`

so I can reference it by name?

#### Jalex Stark (Aug 03 2020 at 18:36):

it's a function of one argument

#### Jalex Stark (Aug 03 2020 at 18:36):

so you can just pass in the argument

#### Jalex Stark (Aug 03 2020 at 18:36):

as in `uparrow X p hp`

#### Kevin Buzzard (Aug 03 2020 at 18:37):

@Iocta :

```
uparrow : Π (X : Type) {P : set X} [_inst_1 : preorder X] (p : X), p ∈ P → set X
```

is exactly the same as

```
uparrow : Π (X : Type) {P : set X} [_inst_1 : preorder X] (p : X) (hp : p ∈ P), set X
```

#### Iocta (Aug 03 2020 at 18:39):

Sorry if I'm being dense, I don't know what this means:

```
example [preorder X] (p : X) (hp: p ∈ P) : is_upper (uparrow X p hp) := sorry
type expected at
is_upper ↥(uparrow X p hp)
term has type
set ↥(uparrow X p hp) → Prop
```

#### Reid Barton (Aug 03 2020 at 18:40):

Check the type of `is_upper`

...

#### Kevin Buzzard (Aug 03 2020 at 18:48):

@Iocta Lean is just using logic here, and you can use logic too to figure out exactly which inputs each function wants, and the error messages explain when you have not given each function the right inputs.

#### Kevin Buzzard (Aug 03 2020 at 18:49):

Hovering over the name of a function will tell you exactly what the inputs it wants are

#### Iocta (Aug 03 2020 at 19:22):

```
variables [preorder X] (p : X) (hp: p ∈ P) (S: uparrow p hp)
-- Why can I say this
example [preorder X] : is_upper (uparrow p hp) := sorry
-- but not this?
example [preorder X] : is_upper S := sorry
```

#### Iocta (Aug 03 2020 at 19:23):

```
type mismatch at application
is_upper S
term
S
has type
↥(uparrow p hp)
but is expected to have type
set ?m_1
```

#### Iocta (Aug 03 2020 at 19:23):

isn't `↥(uparrow p hp)`

a set?

#### Adam Topaz (Aug 03 2020 at 19:24):

The strange arrow means `subtype`

. It's the subtype associated to the set `uparrow _ _`

.

#### Reid Barton (Aug 03 2020 at 19:25):

whatever else is happening, if `is_upper (uparrow p hp)`

makes sense and `S : uparrow p hp`

, then surely `is_upper S`

will almost never make sense!

#### Iocta (Aug 03 2020 at 19:26):

oh I see, they're at different levels

#### Kevin Buzzard (Aug 03 2020 at 19:26):

@Iocta do you know the difference between a type and a term? https://xenaproject.wordpress.com/2020/06/20/mathematics-in-type-theory/

#### Iocta (Aug 03 2020 at 19:26):

yeah, just realized that

#### Kevin Buzzard (Aug 03 2020 at 19:26):

In Lean, if `X : Type`

then `X`

is a type, but if `A : set X`

then `A`

is a term, not a type.

#### Kevin Buzzard (Aug 03 2020 at 19:27):

So even though we might informally think of X as a "set" and A as a "subset" and hence a "set", they are at different levels as you say.

#### Kevin Buzzard (Aug 03 2020 at 19:27):

The weird arrow promotes a term to a type, in the cases when this can be done

#### Kevin Buzzard (Aug 03 2020 at 19:28):

e.g it would promote `A : set X`

to a type called a subtype; to give a term of this subtype you have to give a pair consisting of `x : X`

and then a proof that `x \in A`

.

#### Kevin Buzzard (Aug 03 2020 at 19:28):

But a random term can't be promoted to a type

#### Iocta (Aug 03 2020 at 19:33):

```
example [preorder X] : is_upper (uparrow p hp) := sorry
example [preorder X] : ∀ p ∈ P, is_upper (uparrow p H) := sorry
```

that `H`

is what i was looking for before "does that mean I'm supposed to change it from forall to introducing a specific hp : p \in P so I can reference it by name"

#### Iocta (Aug 03 2020 at 19:54):

Currently `X`

`has_le`

, but I think I mean for `P`

to `has_le`

instead, since the whole point of the exercise is that the ordering of `X`

s is flexible. Therefore do I want to make `P`

a subtype of `X`

that `has_le`

instead of a `set X`

, so then I can say `[preorder P]`

?

#### Kevin Buzzard (Aug 03 2020 at 20:01):

I don't know what you want because I don't know what you're doing

#### Iocta (Aug 03 2020 at 20:07):

I want to talk about "the opposite preorder of P": Given a preorder (P, <=), the opposite is a preorder (P, <=op) having p <=op q iff q <= p

#### Iocta (Aug 03 2020 at 20:08):

which Reid said above is `order_dual`

#### Kevin Buzzard (Aug 03 2020 at 20:08):

#### Reid Barton (Aug 03 2020 at 20:08):

I would just get rid of `P`

(or `X`

)

#### Reid Barton (Aug 03 2020 at 20:09):

er, wait

#### Reid Barton (Aug 03 2020 at 20:09):

I now agree with Kevin

#### Iocta (Aug 03 2020 at 20:09):

haha :-)

#### Reid Barton (Aug 03 2020 at 20:10):

`is_upper`

looks sensible, but why is there a `P`

in `uparrow`

?

#### Kevin Buzzard (Aug 03 2020 at 20:10):

The preorder instance on the dual is https://github.com/leanprover-community/mathlib/blob/c6381aa1175c78083b91732aebefb793156a656a/src/order/basic.lean#L235-L240

#### Iocta (Aug 03 2020 at 20:16):

I was trying to express "P := (X, <=) is a preorder" but maybe that's pointless and I should just say X is orderable in the first place

#### Kevin Buzzard (Aug 03 2020 at 20:17):

`P : set X`

means P is a subset of X, not P=X as a set

#### Iocta (Aug 03 2020 at 20:19):

I get that part; I'll just skip P as suggested

#### Kevin Buzzard (Aug 03 2020 at 20:20):

`[preorder X]`

means "(X,<=) is a preorder"

#### Iocta (Aug 03 2020 at 20:23):

oh. I see

Last updated: May 11 2021 at 23:11 UTC