smul_pos_iff_of_pos_right — Mathlib

English

Under SMulPosStrictMono and SMulPosReflectLT, 0 < a•b iff 0 < a when 0 < b.

Русский

При SMulPosStrictMono и SMulPosReflectLT, 0 < a•b тогда и только тогда, когда 0 < a, если 0 < b.

LaTeX

$$PosSMulStrictMono\\,\\alpha\\,\\beta \\; [SMulPosReflectLT] \\; (hb : 0 < b) \\Rightarrow (0 < a \\cdot b \\iff 0 < a)$$

Lean4

@[simp]
theorem smul_pos_iff_of_pos_right [SMulPosStrictMono α β] [SMulPosReflectLT α β] (hb : 0 < b) : 0 < a • b ↔ 0 < a := by
  simpa only [zero_smul] using smul_lt_smul_iff_of_pos_right hb (a₁ := 0) (a₂ := a)

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