Theorem BddAbove.range_comp_of_nonneg

Modification history

2025-01-16 10:39
Mathlib/Algebra/Order/GroupWithZero/Bounds.lean
feat: split Mathlib/Algebra/Order/Ring/Unbundled/Nonneg (#20703) …
Modified BddAbove.range_comp_of_nonnegView on Github →
2025-01-13 15:16
Mathlib/Algebra/Order/Ring/Unbundled/Nonneg.lean
feat(Algebra/Order/Ring/Unbundled/Nonneg.lean): add boundedness lemmas (#18172) …
Added BddAbove.range_comp_of_nonnegView on Github →