isReduced_iff_not_step — Mathlib

English

IsReduced L1 if and only if for all L2, Red.Step L1 L2 does not hold.

Русский

Редуцированность слова L1 эквивалентна тому, что для всех L2 редукционный шаг L1 → L2 не выполняется.

LaTeX

$$$\operatorname{IsReduced}(L_1) \iff \forall L_2, \neg \operatorname{Red.Step}(L_1,L_2).$$$

Lean4

@[to_additive]
theorem isReduced_iff_not_step : IsReduced L₁ ↔ ∀ L₂, ¬Red.Step L₁ L₂
    where
  mp h _ := h.not_step
  mpr := .of_forall_not_step

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