English
If a < b in WithTop α and n ≠ 0, then a^n < b^n.
Русский
Если a < b в WithTop α и n ≠ 0, то a^n < b^n.
LaTeX
$$$\\\\forall a,b \\in \\mathrm{WithTop} \\\\alpha, a < b \\\\Rightarrow \\\\forall n, n \\neq 0 \\\\Rightarrow a^n < b^n$$$
Lean4
@[gcongr]
protected theorem mul_lt_mul (ha : a₁ < a₂) (hb : b₁ < b₂) : a₁ * b₁ < a₂ * b₂ :=
by
have := posMulStrictMono_iff_mulPosStrictMono.1 ‹_›
lift a₁ to α using ha.lt_top.ne
lift b₁ to α using hb.lt_top.ne
obtain rfl | ha₂ := eq_or_ne a₂ ⊤
· rw [top_mul (by simpa [bot_eq_zero] using hb.bot_lt.ne')]
exact coe_lt_top _
obtain rfl | hb₂ := eq_or_ne b₂ ⊤
· rw [mul_top (by simpa [bot_eq_zero] using ha.bot_lt.ne')]
exact coe_lt_top _
lift a₂ to α using ha₂
lift b₂ to α using hb₂
norm_cast at *
obtain rfl | hb₁ := eq_zero_or_pos b₁
· rw [mul_zero]
exact mul_pos (by simpa [bot_eq_zero] using ha.bot_lt) hb
· exact mul_lt_mul ha hb.le hb₁ (zero_le _)
