step_isSpecial — Mathlib

English

Specialness is preserved by a reduction step: if hs holds for u, then u.step.IsSpecial.

Русский

Свойство специальности сохраняется после шагаReduce: если ws для u, то u.step.IsSpecial.

LaTeX

$$$\\text{IsSpecial}(u) \\Rightarrow \\text{IsSpecial}(u.step)$$$

Lean4

theorem step_isSpecial (hs : u.IsSpecial) : u.step.IsSpecial :=
  by
  dsimp [IsSpecial, step] at hs ⊢
  rw [mul_add, mul_comm u.y u.x, ← hs]
  ring

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