isRightInversion_mul_left_iff — Mathlib

English

A right inversion of w t with respect to t is equivalent to not having a right inversion of w with respect to t.

Русский

Правое инверирование w t относительно t эквивалентно отсутствию правого инверирования w относительно t.

LaTeX

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

Lean4

theorem isRightInversion_mul_left_iff {w : W} : cs.IsRightInversion (w * t) t ↔ ¬cs.IsRightInversion w t :=
  by
  unfold IsRightInversion
  simp only [mul_assoc, ht.mul_self, mul_one, ht, true_and, not_lt]
  constructor
  · exact le_of_lt
  · exact (lt_of_le_of_ne' · (ht.length_mul_left_ne w))

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