For any w : α × Bool, FreeGroup.startsWith w is the set of all elements of FreeGroup α that start with w.

The main theorem Orbit.duplicate proves that applying w⁻¹ to the orbit of x under the action of FreeGroup.startsWith w yields the orbit of x under the action of FreeGroup.startsWith v for every v ≠ w⁻¹ (and the point x).

def FreeGroup.startsWith {α : Type u_1} [DecidableEq α] (w : α × Bool) : Set (FreeGroup α)

All elements of the free Group that start with a certain letter.

theorem FreeGroup.startsWith.ne_one {α : Type u_1} [DecidableEq α] {w : α × Bool} (g : FreeGroup α) (h : g ∈ startsWith w) : g ≠ 1

The neutral element is not contained in one of the startsWith sets.

@[simp]

theorem FreeGroup.startsWith.disjoint_iff_ne {α : Type u_1} [DecidableEq α] {w w' : α × Bool} : Disjoint (startsWith w) (startsWith w') ↔ w ≠ w'

theorem FreeGroup.startsWith.Injective {α : Type u_1} [DecidableEq α] : Function.Injective startsWith

theorem FreeGroup.startsWith_mk_mul {α : Type u_1} [DecidableEq α] {w : α × Bool} (g : FreeGroup α) (h : g ∉ startsWith (w.1, !w.2)) : mk [w] * g ∈ startsWith w

@[implicit_reducible]

instance FreeGroup.instSMulElemStartsWith {α : Type u_1} {X : Type u_2} [DecidableEq α] [MulAction (FreeGroup α) X] {w : α × Bool} : SMul (↑(startsWith w)) X

@[simp]

theorem FreeGroup.startsWith.smul_def {α : Type u_1} {X : Type u_2} [DecidableEq α] [MulAction (FreeGroup α) X] {w : α × Bool} {g : ↑(startsWith w)} {x : X} : g • x = ↑g • x

theorem FreeGroup.Orbit.duplicate {α : Type u_1} {X : Type u_2} [DecidableEq α] [MulAction (FreeGroup α) X] (x : X) (w : α × Bool) : {x_1 : X | ∃ y ∈ MulAction.orbit (↑(startsWith w)) x, (mk [w])⁻¹ • y = x_1} = (⋃ v ∈ {z : α × Bool | z ≠ (w.1, !w.2)}, MulAction.orbit (↑(startsWith v)) x) ∪ {x}

Applying w⁻¹ to the orbit generated by all elements of a free group that start with w yields the orbit generated by all the words that start with every letter except w⁻¹ (and the original point).