rev — Mathlib

English

If L1 reduces to L2, then L2 reduces to the maximal reduction of L1: Red L2 (reduce L1).

Русский

Если L1 редуцируется до L2, то L2 редуцируется до максимального редуктора L1: Red L2 (reduce L1).

LaTeX

$$$$\text{If } \operatorname{Red}(L_1,L_2) \text{ then } \operatorname{Red}(L_2, \operatorname{reduce}(L_1)).$$$$

Lean4

/-- If words `w₁ w₂` are such that `w₁` reduces to `w₂`, then `w₂` reduces to the maximal reduction
  of `w₁`. -/
@[to_additive /-- If words `w₁ w₂` are such that `w₁` reduces to `w₂`, then `w₂` reduces to the
      maximal reduction of `w₁`. -/
    ]
theorem rev (H : Red L₁ L₂) : Red L₂ (reduce L₁) :=
  (reduce.eq_of_red H).symm ▸ reduce.red

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