English
Assume α has a positive multiplication property (PosMulStrictMono). If a > 0 and a ≠ ⊤ in WithTop α, then the map x ↦ a·x is strictly monotone on WithTop α.
Русский
Пусть α удовлетворяет условию PosMulStrictMono. Если a > 0 и a ≠ ⊤ в WithTop α, то отображение x ↦ a·x строго монотонно на WithTop α.
LaTeX
$$$\\\\forall a \\in \\mathrm{WithTop}\\\\,\\alpha,\n(0 < a \\\\land a \\neq \\top) \\\\Rightarrow \\\\text{StrictMono}(\\\\lambda x, a \\\\\\cdot x)$$$
Lean4
protected theorem mul_right_strictMono [PosMulStrictMono α] (h₀ : 0 < a) (hinf : a ≠ ⊤) : StrictMono (a * ·) :=
by
lift a to α using hinf
rintro b c hbc
lift b to α using hbc.ne_top
match c with
| ⊤ => simp [← coe_mul, mul_top h₀.ne']
| (c : α) =>
simp only [coe_pos, coe_lt_coe, ← coe_mul, gt_iff_lt] at *
exact mul_lt_mul_of_pos_left hbc h₀
