inv_pos_iff_one_div_pos'
plain-language theorem explainer
This equivalence equates the positivity of the multiplicative inverse of a real to the positivity of its one-over form. Real analysts normalizing reciprocal inequalities across library versions would cite it for notation stability. The proof is a one-line simp wrapper that rewrites the division notation via the one_div definition.
Claim. For any real number $x$, $0 < x^{-1}$ if and only if $0 < 1/x$.
background
The declaration sits in the compatibility module whose purpose is to collect small alias lemmas that stabilize names across Mathlib versions and reduce duplication. It supplies a named theorem for the equivalence of two reciprocal notations on the reals. No upstream lemmas are imported beyond the core real arithmetic and the one_div definition.
proof idea
The proof is a one-line wrapper that applies the simp tactic with the one_div lemma to equate the two notations.
why it matters
This theorem functions as a compatibility shim that keeps basic positivity facts for reciprocals stable under Mathlib updates. It supports any downstream proof that must check signs of inverses without tying the codebase to a single library version. It touches no core Recognition Science landmarks such as the forcing chain or phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.