one_lt_rpow_of_pos_of_lt_one_of_neg

English

If 0 < x < 1 and z < 0, then 1 < x^z.

Русский

Если 0 < x < 1 и z < 0, тогда 1 < x^z.

LaTeX

$$$ 0 < x < 1 \\land z < 0 \\Rightarrow 1 < x^{z} $$$

Lean4

theorem one_lt_rpow_of_pos_of_lt_one_of_neg {x : ℝ≥0∞} {z : ℝ} (hx1 : 0 < x) (hx2 : x < 1) (hz : z < 0) : 1 < x ^ z :=
  by
  lift x to ℝ≥0 using ne_of_lt (lt_of_lt_of_le hx2 le_top)
  simp only [coe_lt_one_iff, coe_pos] at hx1 hx2 ⊢
  simp [← coe_rpow_of_ne_zero (ne_of_gt hx1), NNReal.one_lt_rpow_of_pos_of_lt_one_of_neg hx1 hx2 hz]

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