not_step_singleton — Mathlib

English

A singleton reduced word cannot be reduced further by a step; a one-letter word does not admit a reduction step.

Русский

Одинокое редуцированное слово не допускает дальнейшего редукционного шага.

LaTeX

$$$ \\forall {p : \\alpha \\times \\mathbb{Bool}}, \\neg \\mathrm{Step}([p])$$$

Lean4

@[to_additive]
theorem not_step_singleton : ∀ {p : α × Bool}, ¬Step [p] L
  | (a, b) => by simp [Step.cons_left_iff, not_step_nil]

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