toPosMulStrictMono — Mathlib

English

Given a CancelMonoidWithZero with a partial order, there is a canonical way to turn PosMulMono into PosMulStrictMono.

Русский

Для CancelMonoidWithZero с частичным порядком существует канонический переход из PosMulMono к PosMulStrictMono.

LaTeX

$$$\text{toPosMulStrictMono} : \text{PosMulMono } \alpha \Rightarrow \text{PosMulStrictMono } \alpha$$$

Lean4

theorem toPosMulStrictMono [PosMulMono α] : PosMulStrictMono α where
  elim := fun x _ _ h => (mul_le_mul_of_nonneg_left h.le x.2.le).lt_of_ne (h.ne ∘ mul_left_cancel₀ x.2.ne')

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