lt_two_mul_self — Mathlib

English

In a ordered semiring with zero less or equal to one and a strict positive multiplier, for any a > 0 we have a < 2a.

Русский

В упорядоченной полускольке с 0 ≤ 1 и положительным множителем, для любого a > 0 имеем a < 2a.

LaTeX

$$$0 \le 1 \Rightarrow \text{MulPosStrictMono}(R) \wedge a > 0 \Rightarrow a < 2a$$$

Lean4

theorem lt_two_mul_self [ZeroLEOneClass R] [MulPosStrictMono R] [NeZero (1 : R)] [AddLeftStrictMono R] (ha : 0 < a) :
    a < 2 * a :=
  lt_mul_of_one_lt_left ha one_lt_two

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