Subset of distinct elements

Stream: new members

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Given X : Set α, does mathlib provide a nice way to say ∀ a b c ∈ X, a ≠ b → a ≠ c → b ≠ c → ...? I.e. to quantify over subsets of distinct elements of X?

[Junyan Xu]

There's docs#Set.Pairwise but not "triplewise" etc.
What you want may be docs#List.sublistsLen (there are Multiset and Finset versions too, but these require X to be finite).

[Eric Wieser]

Or ∀ f : Fin 3 → X, f.Injective → P (f 0) (f 1) (f 2)