reduce_right — Mathlib

English

If h is a reduction from L1 to L2, then Red L1 (reduce L2) holds: reducing after a reduction preserves a reduction relation.

Русский

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

LaTeX

$$$$\text{For } h: \operatorname{Red}(L_1,L_2),\; \operatorname{Red}(L_1, \operatorname{reduce}(L_2)).$$$$

Lean4

@[to_additive]
theorem reduce_right (h : Red L₁ L₂) : Red L₁ (reduce L₂) :=
  reduce.eq_of_red h ▸ reduce.red

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