instPosMulStrictMonoWithZeroOfMulLeftStrictMono

English

An instance that WithZero inherits PosMulStrictMono from MulLeftStrictMono.

Русский

Экземпляр, в котором WithZero наследует PosMulStrictMono от MulLeftStrictMono.

LaTeX

$$InstPosMulStrictMonoWithZeroOfMulLeftStrictMono$$

Lean4

instance {α : Type*} [Mul α] [Preorder α] [MulLeftStrictMono α] : PosMulStrictMono (WithZero α) where
  elim :=
    @fun
      | ⟨(x : α), hx⟩, 0, (b : α), _ => by simpa only [mul_zero] using WithZero.zero_lt_coe _
      | ⟨(x : α), hx⟩, (a : α), (b : α), h => by
        dsimp only at h ⊢
        norm_cast at h ⊢
        exact mul_lt_mul_left' h x

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