not_isLeftInversion_mul_right_iff

English

The negation of left inversion for t w is equivalent to left inversion of w with respect to t.

Русский

Отрицание левому инверсии t w эквивалентно левому инверсию w относительно t.

LaTeX

$$$\neg cs.IsLeftInversion (t \cdot w) t \leftrightarrow cs.IsLeftInversion w t$$$

Lean4

theorem not_isLeftInversion_mul_right_iff {w : W} : ¬cs.IsLeftInversion (t * w) t ↔ cs.IsLeftInversion w t :=
  ht.isLeftInversion_mul_right_iff.not_left

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