one_div_nonneg_of_nonneg'
plain-language theorem explainer
This lemma shows that the reciprocal of any non-negative real number is itself non-negative. Analysts and formalizers working with inequalities across Mathlib versions cite it to avoid name drift in division lemmas. The proof is a one-line tactic that rewrites the division symbol and invokes the standard inverse non-negativity result.
Claim. For any real number $x$ with $x$ nonnegative, the reciprocal satisfies $1/x$ nonnegative.
background
The module supplies small alias lemmas and helpers that stabilize names across Mathlib versions and cut duplication. This result is one such shim for a basic fact of ordered fields: non-negativity is preserved when taking reciprocals, with the library convention that division by zero yields zero. No upstream lemmas are required; the declaration stands alone as a compatibility wrapper.
proof idea
One-line tactic proof. The simpa tactic rewrites the division notation via the one_div definition and then applies the known result that the multiplicative inverse of a nonnegative real is nonnegative.
why it matters
The declaration belongs to the compatibility layer that keeps the Recognition Science formalization portable across Mathlib releases. It supplies a stable name for a standard real-analysis inequality so that downstream proofs do not need to repeat the same rewriting step. No parent theorem in the core chain depends on it directly, but the shim closes a potential source of version-specific breakage.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.