Commit 2023-01-10 21:36 c8c9ce04

View on Github →

feat: port Mathlib.Algebra.Bounds (#1452)

depends on: #1188

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Bounds.lean

added theorem BddAbove.inv

added theorem BddAbove.mul

added theorem BddBelow.inv

added theorem BddBelow.mul

added theorem IsGLB.inv

added theorem IsLUB.inv

added theorem bddAbove_inv

added theorem bddBelow_inv

added theorem csupr_div

added theorem csupᵢ_mul

added theorem isGLB_inv'

added theorem isGLB_inv

added theorem isLUB_inv'

added theorem isLUB_inv

added theorem mul_csupᵢ

added theorem mul_mem_lowerBounds_mul

added theorem mul_mem_upperBounds_mul

added theorem subset_lowerBounds_mul

added theorem subset_upperBounds_mul