toPosMulReflectLE — Mathlib

English

Alternative statement of equivalence between MulPosMono and MulPosStrictMono.

Русский

Альтернативное утверждение эквивалентности MulPosMono и MulPosStrictMono.

LaTeX

$$$MulPosMono\ α \iff MulPosStrictMono\ α$$$

Lean4

theorem toPosMulReflectLE [PosMulReflectLT α] : PosMulReflectLE α where
  elim := fun x _ _ h =>
    h.eq_or_lt.elim (le_of_eq ∘ mul_left_cancel₀ x.2.ne.symm) fun h' => (lt_of_mul_lt_mul_left h' x.2.le).le

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