one_div_pos_of_pos'
Establishes that the reciprocal of a positive real number is positive. Analysts working with inequalities or divisions in real analysis would cite it to maintain sign consistency. The proof is a one-line wrapper that rewrites division and applies the standard inverse positivity result.
claimFor $x$ a real number, if $x > 0$ then $1/x > 0$.
background
The Compat.Mathlib module supplies small alias lemmas and helpers that stabilize names across Mathlib versions and cut duplication. This theorem re-expresses the positivity of the reciprocal using the definition of division as multiplication by the multiplicative inverse.
proof idea
One-line wrapper that applies the inverse positivity lemma after simplifying the division notation.
why it matters in Recognition Science
Supplies a stable name for a basic positivity fact, preventing version-specific breakage in the Recognition Science mathematical layer. It supports any downstream argument that divides by positive reals without introducing extra hypotheses.
scope and limits
- Does not apply to zero or negative reals.
- Does not extend to complex numbers or other fields.
- Does not supply quantitative bounds or rates.
formal statement (Lean)
15theorem one_div_pos_of_pos' {x : ℝ} (hx : 0 < x) : 0 < 1 / x := by
proof body
One-line wrapper that applies simpa.
16 simpa [one_div] using inv_pos.mpr hx
17