mul_left_strictMono — Mathlib

English

If a > 0 and a ≠ ⊤ in WithTop α, then the map x ↦ x·a is strictly monotone on WithTop α.

Русский

Если a > 0 и a ≠ ⊤ в WithTop α, то отображение x ↦ x·a строго монотонно.

LaTeX

$$$\\\\forall a \\in \\mathrm{WithTop}\\\\,\\alpha,\n(0 < a \\\\land a \\neq \\top) \\\\Rightarrow \\\\text{StrictMono}(\\\\lambda x, x \\\\\\cdot a)$$$

Lean4

protected theorem mul_left_strictMono [MulPosStrictMono α] (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, top_mul h₀.ne']
  | (c : α) =>
    simp only [coe_pos, coe_lt_coe, ← coe_mul, gt_iff_lt] at *
    exact mul_lt_mul_of_pos_right hbc h₀

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