not_step_nil

Mathlib.GroupTheory.FreeGroup.Basic

URI: https://scilib.ai/kg/mathlib#FreeGroup.Red.not_step_nil

English

For any L, there is no step from the empty list to L: not Step [] L.

Русский

Для любого L не существует шага от пустого списка к L: not Step [] L.

LaTeX

$$$ \\neg \\mathrm{Step}([],L).$$$

Lean4

@[to_additive]
theorem not_step_nil : ¬Step [] L := by
  generalize h' : [] = L'
  intro h
  rcases h with - | ⟨L₁, L₂⟩
  simp at h'

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru