cutExpand_add_right — Mathlib

English

CutExpand r (s' + t) (s + t) iff CutExpand r s' s (left addition by t cancels).

Русский

CutExpand r (s' + t) (s + t) тогда и только тогда, когда CutExpand r s' s (прибавление слева t отменяется).

LaTeX

$$$\\mathrm{CutExpand}(r)(s' + t,\\, s + t) \\iff \\mathrm{CutExpand}(r)(s',s)$$$

Lean4

theorem cutExpand_add_right {s' s} (t) : CutExpand r (s' + t) (s + t) ↔ CutExpand r s' s := by
  convert cutExpand_add_left t using 2 <;> apply add_comm

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