theorem
proved
one_div_pos_of_pos'
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Compat.Mathlib on GitHub at line 15.
browse module
All declarations in this module, on Recognition.
explainer page
formal source
12
13-- Aliases and small helpers (avoid redefining Mathlib lemmas)
14
15theorem one_div_pos_of_pos' {x : ℝ} (hx : 0 < x) : 0 < 1 / x := by
16 simpa [one_div] using inv_pos.mpr hx
17
18theorem one_div_nonneg_of_nonneg' {x : ℝ} (hx : 0 ≤ x) : 0 ≤ 1 / x := by
19 simpa [one_div] using inv_nonneg.mpr hx
20
21theorem Real.rpow_nonneg_of_nonneg' {x a : ℝ} (hx : 0 ≤ x) : 0 ≤ x ^ a := by
22 simpa using Real.rpow_nonneg hx a
23
24theorem Real.rpow_lt_one_of_pos_of_lt_one' {x y : ℝ}
25 (hx_pos : 0 < x) (hx_lt_one : x < 1) (hy_pos : 0 < y) :
26 x ^ y < 1 := by
27 exact Real.rpow_lt_one hx_pos.le hx_lt_one hy_pos
28
29-- Common simp-normalizations for division forms
30theorem one_div_mul' (x y : ℝ) : (1 / x) * y = y / x := by
31 ring
32
33theorem inv_pos_iff_one_div_pos' {x : ℝ} : (0 < x⁻¹) ↔ (0 < 1 / x) := by
34 simp [one_div]