not_isRightInversion_mul_left_iff

English

The negation of the statement that w t is a right inversion with respect to t is equivalent to w being a right inversion with respect to t.

Русский

Негирование утверждения о том, что w t является правой инверсией относительно t, эквивалентно тому, что w является правой инверсией относительно t.

LaTeX

$$$\neg cs.IsRightInversion (w t) t \leftrightarrow cs.IsRightInversion w t$$$

Lean4

theorem not_isRightInversion_mul_left_iff {w : W} : ¬cs.IsRightInversion (w * t) t ↔ cs.IsRightInversion w t :=
  ht.isRightInversion_mul_left_iff.not_left

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