Distinct variables

Stream: Is there code for X?

[Wouter Smeenk]

What is the best way to have a number of distinct variables? I found https://leanprover-community.github.io/mathlib_docs/data/multiset/nodup.html#multiset.nodup but are there also better ways of doing this?

[Jeremy Salwen]

set.pairwise ne maybe? https://leanprover-community.github.io/mathlib_docs/logic/pairwise.html#set.pairwise

[Kyle Miller]

You could do list.nodup [x1, x2, ...] rather than dealing with multiset.

There's also docs3#set.pairwise_disjoint, where you can write set.pairwise_disjoint {x1, x2, ...} id. Edit: scratch this one, I'm not sure what I was thinking, since disjoint is very different from ne.

[Kyle Miller]

Yeah, set.pairwise {x1, x2, ...} (≠) as well, like Jeremy said. Edit: this doesn't make sense either, as Mario pointed out, since this is trivially true for sets.

[Kyle Miller]

There's also the question of what you mean by a variable. You could also consider an I-indexed family of variables f : I -> X and then add the condition that f is injective if you want them to be distinct.

[Wouter Smeenk]

I would like to be able to prove something like this:

import Mathlib.Logic.Pairwise

variable (x₁ x₂ x₃
          x₄ x₅ x₆
          x₇ x₈ x₉ : ℕ)

example test : Set.Pairwise {x₁, x₂, x₃, x₄, x₅, x₆, x₇, x₈, x₉} (·≠·) → x₁ ≠ x₂ := by sorry

But I cannot really figure out how to do this.

[Mario Carneiro]

it's actually not true

[Mario Carneiro]

because the hypothesis is trivially true:

example : Set.Pairwise {x₁, x₂, x₃, x₄, x₅, x₆, x₇, x₈, x₉} (·≠·) :=
  fun _ _ _ _ h => h

[Mario Carneiro]

(FYI examples don't get names, you want just example not example test)

[Mario Carneiro]

a version more in line with the spirit of your question, and a rather brute-force solution of it, is:

example : List.Pairwise (·≠·) [x₁, x₂, x₃, x₄, x₅, x₆, x₇, x₈, x₉] → x₁ ≠ x₂ := by
  intro h
  simp at h; simp [h]

[Wouter Smeenk]

Oke that works. Thank you! You say brute force. What would be a better way to do this? Edit: I guess you mean the proof of the example. I thought the definition.

[Yury G. Kudryashov]

One more way: (x : Fin 9 → α) (hx : Injective x)