empty_of_word_prod_eq_one — Mathlib

English

If a word w in the H_i maps to the identity under lift f, then w must be the empty word.

Русский

Если слово w в H_i отображается в единицу под действием lift f, то w является пустым словом.

LaTeX

$$$\forall w:\mathrm{Word}(H),\ lift(f)(w.\mathrm{prod})=1 \Rightarrow w=\mathrm{Word.empty}$$$

Lean4

theorem empty_of_word_prod_eq_one {w : Word H} (h : lift f w.prod = 1) : w = Word.empty :=
  by
  by_contra hnotempty
  obtain ⟨i, j, w, rfl⟩ := NeWord.of_word w hnotempty
  exact lift_word_prod_nontrivial_of_not_empty f hcard X hXnonempty hXdisj hpp w h

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