reduce_left — Mathlib

English

If h is a reduction from L1 to L2, then Red L2 (reduce L1) holds: symmetry of reduction under taking the reduced form.

Русский

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

LaTeX

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

Lean4

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

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