Definitions for the main theorem

The complete non-Mathlib vocabulary used in the public statement.

structure SaxlCounterexamples.MainTheorems.FinitePermutationGroup : Type 1

A finite permutation group: a finite group acting faithfully on a finite set.

• G : Type

  The acting group.

• Point : Type

  The type of points on which the group acts.

• group : Group self.G
• action : MulAction self.G self.Point
• finiteGroup : Finite self.G
• finitePoint : Finite self.Point
• faithful : FaithfulSMul self.G self.Point

def SaxlCounterexamples.MainTheorems.FinitePermutationGroup.IsBase (P : FinitePermutationGroup) (B : Set P.Point) : Prop

A set of points is a base if only the identity fixes every point in it.

Equations

• P.IsBase B = ∀ (g : P.G), (∀ x ∈ B, g • x = x) → g = 1

noncomputable def SaxlCounterexamples.MainTheorems.FinitePermutationGroup.baseSize (P : FinitePermutationGroup) : ℕ

The least size of a base. An injective map from Fin n represents an n-element base; existential quantification makes its enumeration irrelevant.

Equations

• P.baseSize = sInf {n : ℕ | ∃ (b : Fin n → P.Point), Function.Injective b ∧ P.IsBase (Set.range b)}

noncomputable def SaxlCounterexamples.MainTheorems.FinitePermutationGroup.saxlGraph (P : FinitePermutationGroup) : SimpleGraph P.Point

The Saxl graph of a finite permutation group. Two distinct points are adjacent exactly when they lie together in a base of minimum size. Thus this is the ordinary Saxl graph at base size two and the generalized Saxl graph at larger base sizes.

Equations

• One or more equations did not get rendered due to their size.