Bounds

📁 Source: Mathlib/Algebra/Order/Group/Pointwise/Bounds.lean

Statistics

Metric	Count
Definitions	0
Theorems add, inv, mul, neg, range_add, range_inv, range_mul, range_neg, add, inv, mul, neg, range_add, range_inv, range_mul, range_neg, add, div, inv, mul, neg, sub, add, div, inv, mul, neg, sub, add, mul, add_mem_lowerBounds_add, add_mem_upperBounds_add, bddAbove_inv, bddAbove_neg, bddBelow_inv, bddBelow_neg, isGLB_inv, isGLB_inv', isGLB_neg, isGLB_neg', isLUB_inv, isLUB_inv', isLUB_neg, isLUB_neg', mul_mem_lowerBounds_mul, mul_mem_upperBounds_mul, subset_lowerBounds_add, subset_lowerBounds_mul, subset_upperBounds_add, subset_upperBounds_mul	50
Total	50

BddAbove

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add 📖	mathematical	BddAbove Preorder.toLE	Set Set.add	—	Set.Nonempty.mono subset_upperBounds_add Set.Nonempty.add
inv 📖	mathematical	BddAbove Preorder.toLE	BddBelow Set Set.inv InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	bddBelow_inv
mul 📖	mathematical	BddAbove Preorder.toLE	Set Set.mul	—	Set.Nonempty.mono subset_upperBounds_mul Set.Nonempty.mul
neg 📖	mathematical	BddAbove Preorder.toLE	BddBelow Set Set.neg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	bddBelow_neg
range_add 📖	—	BddAbove Preorder.toLE Set.range	—	—	range_comp bddAbove_range_prod Monotone.add monotone_fst monotone_snd
range_inv 📖	mathematical	BddAbove Preorder.toLE Set.range	BddBelow InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	BddBelow.range_inv OrderDual.mulLeftMono OrderDual.mulRightMono
range_mul 📖	—	BddAbove Preorder.toLE Set.range	—	—	range_comp bddAbove_range_prod Monotone.mul' monotone_fst monotone_snd
range_neg 📖	mathematical	BddAbove Preorder.toLE Set.range	BddBelow NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	BddBelow.range_neg OrderDual.addLeftMono OrderDual.addRightMono

BddBelow

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add 📖	mathematical	BddBelow Preorder.toLE	Set Set.add	—	Set.Nonempty.mono subset_lowerBounds_add Set.Nonempty.add
inv 📖	mathematical	BddBelow Preorder.toLE	BddAbove Set Set.inv InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	bddAbove_inv
mul 📖	mathematical	BddBelow Preorder.toLE	Set Set.mul	—	Set.Nonempty.mono subset_lowerBounds_mul Set.Nonempty.mul
neg 📖	mathematical	BddBelow Preorder.toLE	BddAbove Set Set.neg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	bddAbove_neg
range_add 📖	—	BddBelow Preorder.toLE Set.range	—	—	BddAbove.range_add OrderDual.addLeftMono OrderDual.addRightMono
range_inv 📖	mathematical	BddBelow Preorder.toLE Set.range	BddAbove InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	range_comp OrderIso.monotone
range_mul 📖	—	BddBelow Preorder.toLE Set.range	—	—	BddAbove.range_mul OrderDual.mulLeftMono OrderDual.mulRightMono
range_neg 📖	mathematical	BddBelow Preorder.toLE Set.range	BddAbove NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	range_comp OrderIso.monotone

IsGLB

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add 📖	mathematical	IsGLB Preorder.toLE	Set Set.add AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	—	IsLUB.add OrderDual.addLeftMono OrderDual.addRightMono
div 📖	mathematical	IsGLB Preorder.toLE IsLUB	Set Set.div DivInvMonoid.toDiv Group.toDivInvMonoid	—	IsLUB.div OrderDual.mulLeftMono OrderDual.mulRightMono
inv 📖	mathematical	IsGLB Preorder.toLE	IsLUB Set Set.inv InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	isLUB_inv'
mul 📖	mathematical	IsGLB Preorder.toLE	Set Set.mul MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid	—	IsLUB.mul OrderDual.mulLeftMono OrderDual.mulRightMono
neg 📖	mathematical	IsGLB Preorder.toLE	IsLUB Set Set.neg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	isLUB_neg'
sub 📖	mathematical	IsGLB Preorder.toLE IsLUB	Set Set.sub SubNegMonoid.toSub AddGroup.toSubNegMonoid	—	IsLUB.sub OrderDual.addLeftMono OrderDual.addRightMono

IsLUB

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add 📖	mathematical	IsLUB Preorder.toLE	Set Set.add AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	—	isLUB_image2_of_isLUB_isLUB OrderIso.to_galoisConnection
div 📖	mathematical	IsLUB Preorder.toLE IsGLB	Set Set.div DivInvMonoid.toDiv Group.toDivInvMonoid	—	div_eq_mul_inv mul IsGLB.inv
inv 📖	mathematical	IsLUB Preorder.toLE	IsGLB Set Set.inv InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	isGLB_inv'
mul 📖	mathematical	IsLUB Preorder.toLE	Set Set.mul MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid	—	isLUB_image2_of_isLUB_isLUB OrderIso.to_galoisConnection
neg 📖	mathematical	IsLUB Preorder.toLE	IsGLB Set Set.neg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	isGLB_neg'
sub 📖	mathematical	IsLUB Preorder.toLE IsGLB	Set Set.sub SubNegMonoid.toSub AddGroup.toSubNegMonoid	—	sub_eq_add_neg add IsGLB.neg

Set.BddAbove

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add 📖	mathematical	BddAbove Preorder.toLE	Set Set.add	—	BddAbove.add
mul 📖	mathematical	BddAbove Preorder.toLE	Set Set.mul	—	BddAbove.mul

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_mem_lowerBounds_add 📖	mathematical	Set Set.instMembership lowerBounds Preorder.toLE	Set.add	—	add_mem_upperBounds_add OrderDual.addLeftMono OrderDual.addRightMono
add_mem_upperBounds_add 📖	mathematical	Set Set.instMembership upperBounds Preorder.toLE	Set.add	—	Set.forall_mem_image2 add_le_add
bddAbove_inv 📖	mathematical	—	BddAbove Preorder.toLE Set Set.inv InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid BddBelow	—	OrderIso.bddAbove_preimage
bddAbove_neg 📖	mathematical	—	BddAbove Preorder.toLE Set Set.neg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid BddBelow	—	OrderIso.bddAbove_preimage
bddBelow_inv 📖	mathematical	—	BddBelow Preorder.toLE Set Set.inv InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid BddAbove	—	OrderIso.bddBelow_preimage
bddBelow_neg 📖	mathematical	—	BddBelow Preorder.toLE Set Set.neg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid BddAbove	—	OrderIso.bddBelow_preimage
isGLB_inv 📖	mathematical	—	IsGLB Preorder.toLE Set Set.inv InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid IsLUB	—	OrderIso.isGLB_preimage
isGLB_inv' 📖	mathematical	—	IsGLB Preorder.toLE Set Set.inv InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid IsLUB	—	OrderIso.isGLB_preimage'
isGLB_neg 📖	mathematical	—	IsGLB Preorder.toLE Set Set.neg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid IsLUB	—	OrderIso.isGLB_preimage
isGLB_neg' 📖	mathematical	—	IsGLB Preorder.toLE Set Set.neg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid IsLUB	—	OrderIso.isGLB_preimage'
isLUB_inv 📖	mathematical	—	IsLUB Preorder.toLE Set Set.inv InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid IsGLB	—	OrderIso.isLUB_preimage
isLUB_inv' 📖	mathematical	—	IsLUB Preorder.toLE Set Set.inv InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid IsGLB	—	OrderIso.isLUB_preimage'
isLUB_neg 📖	mathematical	—	IsLUB Preorder.toLE Set Set.neg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid IsGLB	—	OrderIso.isLUB_preimage
isLUB_neg' 📖	mathematical	—	IsLUB Preorder.toLE Set Set.neg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid IsGLB	—	OrderIso.isLUB_preimage'
mul_mem_lowerBounds_mul 📖	mathematical	Set Set.instMembership lowerBounds Preorder.toLE	Set.mul	—	mul_mem_upperBounds_mul OrderDual.mulLeftMono OrderDual.mulRightMono
mul_mem_upperBounds_mul 📖	mathematical	Set Set.instMembership upperBounds Preorder.toLE	Set.mul	—	Set.forall_mem_image2 mul_le_mul'
subset_lowerBounds_add 📖	mathematical	—	Set Set.instHasSubset Set.add lowerBounds Preorder.toLE	—	subset_upperBounds_add OrderDual.addLeftMono OrderDual.addRightMono
subset_lowerBounds_mul 📖	mathematical	—	Set Set.instHasSubset Set.mul lowerBounds Preorder.toLE	—	subset_upperBounds_mul OrderDual.mulLeftMono OrderDual.mulRightMono
subset_upperBounds_add 📖	mathematical	—	Set Set.instHasSubset Set.add upperBounds Preorder.toLE	—	Set.image2_subset_iff add_mem_upperBounds_add
subset_upperBounds_mul 📖	mathematical	—	Set Set.instHasSubset Set.mul upperBounds Preorder.toLE	—	Set.image2_subset_iff mul_mem_upperBounds_mul

---

← Back to Index