lift_word_prod_nontrivial_of_other_i

English

If w is a NeWord over H with i = j (a loop) then lift f w.prod ≠ 1, i.e., the lifted word is nontrivial.

Русский

Если w — NeWord над H с i = j (петля), то lift f w.prod ≠ 1, то есть полученное изображение слова ненулевое.

LaTeX

$$$$\\text{lift}(f)\\; w.\\text{prod} \\neq 1.$$$$

Lean4

theorem lift_word_prod_nontrivial_of_other_i {i j k} (w : NeWord H i j) (hhead : k ≠ i) (hlast : k ≠ j) :
    lift f w.prod ≠ 1 := by
  intro heq1
  have : X k ⊆ X i := by simpa [heq1] using lift_word_ping_pong f X hpp w hlast.symm
  obtain ⟨x, hx⟩ := hXnonempty k
  exact (hXdisj hhead).le_bot ⟨hx, this hx⟩

Похожие утверждения