English
Under ping-pong hypotheses, the action lift(f) of a reduced word w moves the set X_k inside X_i along the word, i.e., lift f w.prod · X_k ⊆ X_i.
Русский
При допущениях пинг-понг действие lift(f) над редуцированным словом w перемещает множество X_k в X_i, то есть lift f w.prod · X_k ⊆ X_i.
LaTeX
$$$$\\text{lift}(f)\\; w.\\text{prod} \\;\\cdot X_k \\subseteq X_i.$$$$
Lean4
theorem lift_word_ping_pong {i j k} (w : NeWord H i j) (hk : j ≠ k) : lift f w.prod • X k ⊆ X i := by
induction w generalizing k with
| singleton x hne_one => simpa using hpp hk _ hne_one
| @append i j k l w₁ hne w₂ hIw₁ hIw₂ =>
calc
lift f (NeWord.append w₁ hne w₂).prod • X k = lift f w₁.prod • lift f w₂.prod • X k := by
simp [MulAction.mul_smul]
_ ⊆ lift f w₁.prod • X _ := (smul_set_subset_smul_set_iff.mpr (hIw₂ hk))
_ ⊆ X i := hIw₁ hne
