Generalized Saxl adjacency

The generalized adjacency definition stores the two displayed vertices in the first two positions of an ordered base. This file shows that the order is irrelevant: generalized adjacency is exactly membership of two distinct vertices in a common set-like base of the required size.

theorem Saxl.generalizedAdjacent_iff_mem_base (G : Type u_1) (Ω : Type u_2) [Group G] [MulAction G Ω] (tail : ℕ) (x y : Ω) : GeneralizedAdjacent G Ω tail x y ↔ x ≠ y ∧ ∃ (b : Fin (tail + 2) → Ω), IsSetBaseTuple G Ω b ∧ x ∈ Set.range b ∧ y ∈ Set.range b

Two vertices are generalized-adjacent exactly when they are distinct members of a common base of size tail + 2.