wordProd_surjective — Mathlib

English

The mapping that sends a word to its product is surjective onto the group W.

Русский

Отображение, отправляющее слово в его произведение, сюръективно на группу W.

LaTeX

$$$\\\\text{Surjective}(\\\\pi\\\\;\\\\text{wordProd})$$$

Lean4

theorem wordProd_surjective : Surjective cs.wordProd := by
  intro w
  apply cs.simple_induction_left w
  · use []
    rw [wordProd_nil]
  · rintro _ i ⟨ω, rfl⟩
    use i :: ω
    rw [wordProd_cons]

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