## Stream: Is there code for X?

### Topic: distinct

#### Adam Topaz (Feb 19 2021 at 18:21):

Suppose I have a type $\alpha$ and three terms $x,y,z : \alpha$. What's the idiomatic way to say that $x,y,z$ are distinct?

#### Adam Topaz (Feb 19 2021 at 18:25):

My inclination is to be tricky with matrices:

import data.matrix.notation

def distinct {α : Type*} (x y z : α) := function.injective ![x,y,z]


#### Kevin Buzzard (Feb 19 2021 at 18:31):

This came up on the discord and whatever the idiomatic way is, it was generally agreed that the most helpful way was just x \ne y \and y \ne z \and z \ne x. A more fun question: if alpha is linearly ordered and your goal is S_3-invariant, how do you now prove WLOG x<y<z?

#### Adam Topaz (Feb 19 2021 at 18:32):

Okay, but now what if I have 5 elements?

#### Adam Topaz (Feb 19 2021 at 18:32):

I don't want to write too many things

#### Eric Wieser (Feb 19 2021 at 18:32):

Possibly [x,y,z].pairwise (≠)

#### Eric Wieser (Feb 19 2021 at 18:33):

Which should still give you helpful induction principles

#### Adam Topaz (Feb 19 2021 at 18:35):

I would still like a smaller proof, but this isn't too bad:

import data.matrix.notation

example {α : Type*} {a b c d e f g : α} (cond : function.injective ![a,b,c,d,e,f,g]) : c ≠ g :=
cond.ne \$ show (2 : fin 7) ≠ 6, by dec_trivial


#### Kevin Buzzard (Feb 19 2021 at 19:26):

Do you ever really have 5 elements in practice?

#### Adam Topaz (Feb 19 2021 at 19:28):

I can get by with 3, but I might need 5 in the future :)

#### Adam Topaz (Feb 19 2021 at 19:28):

I don't think I'll ever need 6 though.

#### Adam Topaz (Feb 19 2021 at 19:31):

This all started with the following lemma which I'm working on for some stuff with projective geometry:

lemma exists_unique_rep_of_colinear {x y z : proj K V} {v : V} :
x.is_rep v → colinear x y z → (function.injective ![x,y,z]) →
∃! (w : V), y.is_rep w ∧ z.is_rep (v + w) := sorry


#### Adam Topaz (Feb 19 2021 at 19:31):

(in some sense, this is the key lemma that makes the fundamental theorem of projective geometry actually work.)

Last updated: May 16 2021 at 05:21 UTC