one_le_rpow_of_pos_of_le_one_of_neg

English

If 0 < x and x ≤ 1 and z < 0, then 1 ≤ x^{z}.

Русский

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

LaTeX

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

Lean4

theorem one_le_rpow_of_pos_of_le_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_le_of_lt hx2 coe_lt_top)
  simp only [coe_le_one_iff, coe_pos] at hx1 hx2 ⊢
  simp [← coe_rpow_of_ne_zero (ne_of_gt hx1), NNReal.one_le_rpow_of_pos_of_le_one_of_nonpos hx1 hx2 (le_of_lt hz)]

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