## Stream: maths

### Topic: monotonic isomorphism between finite sets

#### Chris Hughes (Aug 18 2018 at 18:32):

I'm looking for a lexicographic total order on fin a × fin b and a proof that's it's isomorphic to the lexicographic total order on fin b × fin a. Is this easy in lean?

No longer needed

#### Chris Hughes (Aug 21 2018 at 10:01):

Turns out I do need it after all. I need a linear order isomorphism between any two totally ordered types of the same size. Is that anywhere in lean? Seems like the sort of thing that might have come up doing ordinals.

#### Johan Commelin (Aug 21 2018 at 10:09):

I have no idea whether this is in Lean. Also, I'm not a master of finsets, like you are. But my initial attempt would be to prove this by induction. Construct a map to fin n. If the cardinality is 0, then it's easy. If it is k+1 construct a map to fin k+1 by sending the largest element to k.

#### Johan Commelin (Aug 21 2018 at 10:16):

Do you in fact also want to prove that the linear order isom is unique?

#### Chris Hughes (Aug 21 2018 at 10:20):

I don't care if it's unique I don't think.

#### Mario Carneiro (Aug 21 2018 at 11:40):

I need a linear order isomorphism between any two totally ordered types of the same size

This isn't true for all types, e.g. nat and int are not order isomorphic

#### Mario Carneiro (Aug 21 2018 at 11:41):

This fact for finite linear orders is a special case of the uniqueness of well orders in the finite case

#### Kevin Buzzard (Aug 21 2018 at 11:47):

He's only interested in finite types surely

I do mean finite

#### Kevin Buzzard (Aug 21 2018 at 11:59):

So the question is "is existence and uniqueness (up to permutation) of a total order on a finite type in Lean"?

#### Mario Carneiro (Aug 21 2018 at 12:01):

ord n essentially imposes a well order on any set (or the well order theorem directly), which gives you the existence part

#### Chris Hughes (Aug 21 2018 at 12:02):

The uniqueness is what I care about.

#### Mario Carneiro (Aug 21 2018 at 12:11):

A linear order of a finite set is a well order, so you get an embedding of each order into ordinal; the cardinals for these orders is equal so you have uniqueness by ord_nat and hence an order isomorphism

#### Mario Carneiro (Aug 21 2018 at 12:11):

(this is probably an excessively high powered proof)

#### Kenny Lau (Aug 21 2018 at 12:30):

I'm still struggling with something like

noncomputable def something : @order_iso (α) (fin $fintype.card α) (<) (<) := classical.choice$ ordinal.type_eq.1 $(ordinal.fintype_card (<)).trans (ordinal.lift_type_fin$ fintype.card α).symm

#### Kenny Lau (Aug 21 2018 at 12:39):

oh and my incomplete code (posting here because I don't want to work with it now):

#### Kenny Lau (Aug 21 2018 at 12:39):

import set_theory.ordinal

universes u v w

variables (α : Type u) [fintype α] [linear_order α]
variables (β : Type v) [has_lt β] [is_well_order β (<)]
variables (γ : Type w)

instance is_well_order_of_fintype : is_well_order α (<) :=
{ wf := sorry }

@[simp] lemma ulift_up_eq (x y : γ) : ulift.up x = ulift.up y  x = y :=
ulift.up.inj, congr_arg _⟩

instance ulift.is_well_order : is_well_order (ulift.{u v} β) (equiv.ulift.to_fun ⁻¹'o has_lt.lt) :=
{ trans := λ x y z Hxy Hyz, @is_trans.trans β (<) _ x y z Hxy Hyz,
irrefl := λ x H, is_irrefl.irrefl (<) x H,
trichotomous := λ x y, by simpa using is_trichotomous.trichotomous (<) x y,
wf := inv_image.wf _ $is_well_order.wf _ } noncomputable def something : @order_iso (α) (fin$ fintype.card α) (<) (<) :=
classical.choice $ordinal.type_eq.1$ (ordinal.fintype_card (<)).trans (ordinal.lift_type_fin \$ fintype.card α).symm
#check cardinal.ord_nat
#check something

Last updated: May 11 2021 at 16:22 UTC