## Stream: new members

### Topic: orders on products

#### Alistair Tucker (Dec 08 2018 at 19:06):

I want definitions like

instance prod_has_le {α β : Type} [has_le α] [has_le β] : has_le (prod α β) :=
{ le            := λ a b, a.1 ≤ b.1 ∧ a.2 ≤ b.2 }

instance prod_preorder {α β : Type} [preorder α] [preorder β] : preorder (prod α β) :=
{ le_refl       := λ a, ⟨le_refl a.1, le_refl a.2⟩,
le_trans      := λ a b c h₁ h₂, ⟨le_trans h₁.1 h₂.1, le_trans h₁.2 h₂.2⟩,
.. prod_has_le }

instance prod_partial_order {α β : Type} [partial_order α] [partial_order β] : partial_order (prod α β) :=
{ le_antisymm   := λ a b h₁ h₂, prod.ext (le_antisymm h₁.1 h₂.1) (le_antisymm h₁.2 h₂.2),
.. prod_preorder }


(At the moment just for ℕ × ℕ, Cauchy sequences and contraction mapping theorem, but probably for more later on.)

These don't seem already to be in mathlib, so should I assume there is some good reason to exclude them? And if so, can I use some namespace trick to define them 'locally'?

#### Kevin Buzzard (Dec 08 2018 at 19:08):

I think attribute local instance works for something which is already defined.

#### Kevin Buzzard (Dec 08 2018 at 19:09):

For example this is from TPIL:

open classical
local attribute [instance] prop_decidable


(after prop_decidable has been defined)

#### Kevin Buzzard (Dec 08 2018 at 19:12):

"However, such commands can often be prefixed with the local modifier, which indicates that they only have effect until the current section or namespace is closed, or until the end of the current file."

#### Alistair Tucker (Dec 08 2018 at 19:14):

Thanks, I'll do that then.

#### Kevin Buzzard (Dec 08 2018 at 19:19):

It would not surprise me if there were a trick to do it all in one go. Does local instance... not work?

#### Kevin Buzzard (Dec 08 2018 at 19:19):

Oh! Do you need to import pi_instances or something? Maybe they're there?

#### Alistair Tucker (Dec 08 2018 at 20:52):

Hmm possibly. I didn't know about pi_instances.

import algebra.pi_instances

def a : bool → ℕ := λ i, if i then 1 else 2
def b : bool → ℕ := λ i, if i then 3 else 4

#check a ≤ b


#### Kevin Buzzard (Dec 08 2018 at 20:54):

import algebra.pi_instances

example {α β : Type} [partial_order α] [partial_order β] :
partial_order (α × β) := by apply_instance -- fails


I thought it might work out of the box. But no.

#### Kevin Buzzard (Dec 08 2018 at 20:55):

Maybe the reason it's not an instance is that some people might want to use lex order in some cases

Last updated: May 06 2021 at 22:13 UTC