Documentation Verification Report

Basic

📁 Source: Mathlib/Algebra/Order/Interval/Basic.lean

Statistics

MetricCount
DefinitionsaddCommMonoid, addZeroClass, commMonoid, divisionCommMonoid, length, mulOneClass, subtractionCommMonoid, evalIntervalLength, evalNonemptyIntervalLength, addCommMonoid, commMonoid, divisionCommMonoid, hasNSMul, hasPow, instCommSemiringOfCanonicallyOrderedAdd, instNatCast, length, subtractionCommMonoid, instAddInterval, instAddNonemptyInterval, instDivInterval, instDivNonemptyInterval, instInvInterval, instInvNonemptyInterval, instMulInterval, instMulNonemptyInterval, instNegInterval, instNegNonemptyInterval, instOneNonemptyInterval, instSubInterval, instSubNonemptyInterval, instZeroNonemptyInterval
32
Theoremsadd_bot, add_eq_zero_iff, bot_add, bot_div, bot_mul, bot_ne_one, bot_ne_zero, bot_nsmul, bot_pow, bot_sub, coe_one, coe_zero, div_bot, inv_bot, length_add_le, length_neg, length_nonneg, length_pure, length_sub_le, length_sum_le, length_zero, mul_bot, mul_eq_one_iff, neg_bot, one_mem_one, one_ne_bot, pure_one, pure_zero, sub_bot, zero_mem_zero, zero_ne_bot, add_eq_zero_iff, coe_add_interval, coe_div_interval, coe_inv_interval, coe_mul_interval, coe_neg_interval, coe_nsmul_interval, coe_one, coe_one_interval, coe_pow_interval, coe_sub_interval, coe_zero, coe_zero_interval, div_mem_div, fst_add, fst_div, fst_inv, fst_mul, fst_natCast, fst_neg, fst_nsmul, fst_one, fst_pow, fst_sub, fst_zero, inv_mem_inv, inv_pure, length_add, length_neg, length_nonneg, length_pure, length_sub, length_sum, length_zero, mul_eq_one_iff, neg_mem_neg, neg_pure, one_mem_one, pure_add_pure, pure_div_pure, pure_mul_pure, pure_natCast, pure_nsmul, pure_one, pure_pow, pure_sub_pure, pure_zero, snd_add, snd_div, snd_inv, snd_mul, snd_natCast, snd_neg, snd_nsmul, snd_one, snd_pow, snd_sub, snd_zero, sub_mem_sub, toProd_add, toProd_mul, toProd_nsmul, toProd_one, toProd_pow, toProd_zero, zero_mem_zero
97
Total129

Interval

Definitions

NameCategoryTheorems
addCommMonoid 📖CompOp
3 mathmath: NonemptyInterval.coe_nsmul_interval, length_sum_le, bot_nsmul
addZeroClass 📖CompOp
commMonoid 📖CompOp
2 mathmath: NonemptyInterval.coe_pow_interval, bot_pow
divisionCommMonoid 📖CompOp
length 📖CompOp
7 mathmath: length_sub_le, length_sum_le, length_nonneg, length_zero, length_neg, length_add_le, length_pure
mulOneClass 📖CompOp
subtractionCommMonoid 📖CompOp

Theorems

NameKindAssumesProvesValidatesDepends On
add_bot 📖mathematicalInterval
Preorder.toLE
instAddInterval
Bot.bot
WithBot.bot
NonemptyInterval
WithBot.map₂_bot_right
add_eq_zero_iff 📖mathematicalInterval
Preorder.toLE
PartialOrder.toPreorder
instAddInterval
AddZero.toAdd
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
SubNegMonoid.toAddMonoid
AddGroup.toSubNegMonoid
AddCommGroup.toAddGroup
IsOrderedAddMonoid.toAddLeftMono
AddCommGroup.toAddCommMonoid
covariant_swap_add_of_covariant_add
AddCommMonoid.toAddCommSemigroup
WithBot.zero
NonemptyInterval
instZeroNonemptyInterval
NegZeroClass.toZero
SubNegZeroMonoid.toNegZeroClass
SubtractionMonoid.toSubNegZeroMonoid
SubtractionCommMonoid.toSubtractionMonoid
AddCommGroup.toDivisionAddCommMonoid
pure
IsOrderedAddMonoid.toAddLeftMono
covariant_swap_add_of_covariant_add
bot_add
WithBot.bot_ne_zero
bot_ne_pure
Zero.instNonempty
add_bot
NonemptyInterval.coe_eq_pure
NonemptyInterval.add_eq_zero_iff
bot_add 📖mathematicalInterval
Preorder.toLE
instAddInterval
Bot.bot
WithBot.bot
NonemptyInterval
WithBot.map₂_bot_left
bot_div 📖mathematicalInterval
Preorder.toLE
instDivInterval
Bot.bot
WithBot.bot
NonemptyInterval
WithBot.map₂_bot_left
bot_mul 📖mathematicalInterval
Preorder.toLE
instMulInterval
Bot.bot
WithBot.bot
NonemptyInterval
WithBot.map₂_bot_left
bot_ne_one 📖bot_ne_pure
bot_ne_zero 📖bot_ne_pure
bot_nsmul 📖mathematicalInterval
Preorder.toLE
PartialOrder.toPreorder
AddMonoid.toNatSMul
AddCommMonoid.toAddMonoid
addCommMonoid
Bot.bot
WithBot.bot
NonemptyInterval
add_bot
IsOrderedAddMonoid.toAddLeftMono
bot_pow 📖mathematicalInterval
Preorder.toLE
PartialOrder.toPreorder
Monoid.toNatPow
CommMonoid.toMonoid
commMonoid
Bot.bot
WithBot.bot
NonemptyInterval
mul_bot
IsOrderedMonoid.toMulLeftMono
bot_sub 📖mathematicalInterval
Preorder.toLE
instSubInterval
Bot.bot
WithBot.bot
NonemptyInterval
WithBot.map₂_bot_left
coe_one 📖mathematicalSetLike.coe
Interval
Preorder.toLE
PartialOrder.toPreorder
setLike
WithBot.one
NonemptyInterval
instOneNonemptyInterval
Set
Set.one
Set.Icc_self
coe_zero 📖mathematicalSetLike.coe
Interval
Preorder.toLE
PartialOrder.toPreorder
setLike
WithBot.zero
NonemptyInterval
instZeroNonemptyInterval
Set
Set.zero
Set.Icc_self
div_bot 📖mathematicalInterval
Preorder.toLE
instDivInterval
Bot.bot
WithBot.bot
NonemptyInterval
WithBot.map₂_bot_right
inv_bot 📖mathematicalInterval
Preorder.toLE
PartialOrder.toPreorder
instInvInterval
Bot.bot
WithBot.bot
NonemptyInterval
length_add_le 📖mathematicalPreorder.toLE
PartialOrder.toPreorder
length
Interval
instAddInterval
AddCommMagma.toAdd
AddCommSemigroup.toAddCommMagma
AddCommMonoid.toAddCommSemigroup
AddCommGroup.toAddCommMonoid
IsOrderedAddMonoid.toAddLeftMono
covariant_swap_add_of_covariant_add
IsOrderedAddMonoid.toAddLeftMono
covariant_swap_add_of_covariant_add
IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT
AddLeftCancelSemigroup.toIsLeftCancelAdd
IsOrderedCancelAddMonoid.toAddLeftReflectLT
IsOrderedAddMonoid.toIsOrderedCancelAddMonoid
WithBot.add_bot
IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT
AddRightCancelSemigroup.toIsRightCancelAdd
contravariant_swap_add_of_contravariant_add
Eq.le
NonemptyInterval.length_add
length_neg 📖mathematicallength
Interval
Preorder.toLE
PartialOrder.toPreorder
instNegInterval
NonemptyInterval.length_neg
length_nonneg 📖mathematicalPreorder.toLE
PartialOrder.toPreorder
NegZeroClass.toZero
SubNegZeroMonoid.toNegZeroClass
SubtractionMonoid.toSubNegZeroMonoid
SubtractionCommMonoid.toSubtractionMonoid
AddCommGroup.toDivisionAddCommMonoid
length
le_rfl
NonemptyInterval.length_nonneg
length_pure 📖mathematicallength
pure
PartialOrder.toPreorder
NegZeroClass.toZero
SubNegZeroMonoid.toNegZeroClass
SubtractionMonoid.toSubNegZeroMonoid
SubtractionCommMonoid.toSubtractionMonoid
AddCommGroup.toDivisionAddCommMonoid
NonemptyInterval.length_pure
length_sub_le 📖mathematicalPreorder.toLE
PartialOrder.toPreorder
length
Interval
instSubInterval
AddCommMonoid.toAddCommSemigroup
AddCommGroup.toAddCommMonoid
SubNegMonoid.toSub
AddGroup.toSubNegMonoid
AddCommGroup.toAddGroup
AddGroup.toOrderedSub
covariant_swap_add_of_covariant_add
IsOrderedAddMonoid.toAddLeftMono
AddCommMagma.toAdd
AddCommSemigroup.toAddCommMagma
AddGroup.toOrderedSub
covariant_swap_add_of_covariant_add
IsOrderedAddMonoid.toAddLeftMono
sub_eq_add_neg
length_neg
length_add_le
length_sum_le 📖mathematicalPreorder.toLE
PartialOrder.toPreorder
length
Finset.sum
Interval
addCommMonoid
AddCommGroup.toAddCommMonoid
Finset.le_sum_of_subadditive
Eq.le
length_zero
length_add_le
length_zero 📖mathematicallength
Interval
Preorder.toLE
PartialOrder.toPreorder
WithBot.zero
NonemptyInterval
instZeroNonemptyInterval
NegZeroClass.toZero
SubNegZeroMonoid.toNegZeroClass
SubtractionMonoid.toSubNegZeroMonoid
SubtractionCommMonoid.toSubtractionMonoid
AddCommGroup.toDivisionAddCommMonoid
length_pure
mul_bot 📖mathematicalInterval
Preorder.toLE
instMulInterval
Bot.bot
WithBot.bot
NonemptyInterval
WithBot.map₂_bot_right
mul_eq_one_iff 📖mathematicalInterval
Preorder.toLE
PartialOrder.toPreorder
instMulInterval
MulOne.toMul
MulOneClass.toMulOne
Monoid.toMulOneClass
DivInvMonoid.toMonoid
Group.toDivInvMonoid
CommGroup.toGroup
IsOrderedMonoid.toMulLeftMono
CommGroup.toCommMonoid
covariant_swap_mul_of_covariant_mul
CommMonoid.toCommSemigroup
WithBot.one
NonemptyInterval
instOneNonemptyInterval
InvOneClass.toOne
DivInvOneMonoid.toInvOneClass
DivisionMonoid.toDivInvOneMonoid
DivisionCommMonoid.toDivisionMonoid
CommGroup.toDivisionCommMonoid
pure
IsOrderedMonoid.toMulLeftMono
covariant_swap_mul_of_covariant_mul
bot_mul
One.instNonempty
mul_bot
NonemptyInterval.mul_eq_one_iff
neg_bot 📖mathematicalInterval
Preorder.toLE
PartialOrder.toPreorder
instNegInterval
Bot.bot
WithBot.bot
NonemptyInterval
one_mem_one 📖mathematicalInterval
Preorder.toLE
PartialOrder.toPreorder
SetLike.instMembership
setLike
WithBot.one
NonemptyInterval
instOneNonemptyInterval
le_rfl
one_ne_bot 📖pure_ne_bot
pure_one 📖mathematicalpure
Interval
Preorder.toLE
WithBot.one
NonemptyInterval
instOneNonemptyInterval
pure_zero 📖mathematicalpure
Interval
Preorder.toLE
WithBot.zero
NonemptyInterval
instZeroNonemptyInterval
sub_bot 📖mathematicalInterval
Preorder.toLE
instSubInterval
Bot.bot
WithBot.bot
NonemptyInterval
WithBot.map₂_bot_right
zero_mem_zero 📖mathematicalInterval
Preorder.toLE
PartialOrder.toPreorder
SetLike.instMembership
setLike
WithBot.zero
NonemptyInterval
instZeroNonemptyInterval
le_rfl
zero_ne_bot 📖pure_ne_bot

Mathlib.Meta.Positivity

Definitions

NameCategoryTheorems
evalIntervalLength 📖CompOp
evalNonemptyIntervalLength 📖CompOp

NonemptyInterval

Definitions

NameCategoryTheorems
addCommMonoid 📖CompOp
1 mathmath: length_sum
commMonoid 📖CompOp
divisionCommMonoid 📖CompOp
hasNSMul 📖CompOp
5 mathmath: toProd_nsmul, coe_nsmul_interval, pure_nsmul, fst_nsmul, snd_nsmul
hasPow 📖CompOp
5 mathmath: pure_pow, toProd_pow, coe_pow_interval, snd_pow, fst_pow
instCommSemiringOfCanonicallyOrderedAdd 📖CompOp
instNatCast 📖CompOp
3 mathmath: fst_natCast, pure_natCast, snd_natCast
length 📖CompOp
7 mathmath: length_zero, length_nonneg, length_add, length_sum, length_sub, length_pure, length_neg
subtractionCommMonoid 📖CompOp

Theorems

NameKindAssumesProvesValidatesDepends On
add_eq_zero_iff 📖mathematicalNonemptyInterval
Preorder.toLE
PartialOrder.toPreorder
instAddNonemptyInterval
AddZero.toAdd
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
SubNegMonoid.toAddMonoid
AddGroup.toSubNegMonoid
AddCommGroup.toAddGroup
IsOrderedAddMonoid.toAddLeftMono
AddCommGroup.toAddCommMonoid
covariant_swap_add_of_covariant_add
AddCommMonoid.toAddCommSemigroup
instZeroNonemptyInterval
NegZeroClass.toZero
SubNegZeroMonoid.toNegZeroClass
SubtractionMonoid.toSubNegZeroMonoid
SubtractionCommMonoid.toSubtractionMonoid
AddCommGroup.toDivisionAddCommMonoid
pure
IsOrderedAddMonoid.toAddLeftMono
covariant_swap_add_of_covariant_add
add_le_add_iff_of_ge
IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono
AddLeftCancelSemigroup.toIsLeftCancelAdd
IsRightCancelAdd.addRightStrictMono_of_addRightMono
AddRightCancelSemigroup.toIsRightCancelAdd
fst_le_snd
Eq.le
ext_iff
ext
pure_add_pure
pure_zero
coe_add_interval 📖mathematicalWithBot.some
NonemptyInterval
Preorder.toLE
instAddNonemptyInterval
WithBot
instAddInterval
coe_div_interval 📖mathematicalWithBot.some
NonemptyInterval
Preorder.toLE
instDivNonemptyInterval
WithBot
instDivInterval
coe_inv_interval 📖mathematicalWithBot.some
NonemptyInterval
Preorder.toLE
PartialOrder.toPreorder
instInvNonemptyInterval
WithBot
instInvInterval
coe_mul_interval 📖mathematicalWithBot.some
NonemptyInterval
Preorder.toLE
instMulNonemptyInterval
WithBot
instMulInterval
coe_neg_interval 📖mathematicalWithBot.some
NonemptyInterval
Preorder.toLE
PartialOrder.toPreorder
instNegNonemptyInterval
WithBot
instNegInterval
coe_nsmul_interval 📖mathematicalWithBot.some
NonemptyInterval
Preorder.toLE
PartialOrder.toPreorder
hasNSMul
AddCommMonoid.toAddMonoid
IsOrderedAddMonoid.toAddLeftMono
covariant_swap_add_of_covariant_add
AddCommMonoid.toAddCommSemigroup
WithBot
AddMonoid.toNatSMul
Interval.addCommMonoid
map_nsmul
AddMonoidHom.instAddMonoidHomClass
coe_zero_interval
coe_add_interval
IsOrderedAddMonoid.toAddLeftMono
coe_one 📖mathematicalSetLike.coe
NonemptyInterval
Preorder.toLE
PartialOrder.toPreorder
setLike
instOneNonemptyInterval
Set
Set.one
coe_pure
coe_one_interval 📖mathematicalWithBot.some
NonemptyInterval
Preorder.toLE
instOneNonemptyInterval
WithBot
WithBot.one
coe_pow_interval 📖mathematicalWithBot.some
NonemptyInterval
Preorder.toLE
PartialOrder.toPreorder
hasPow
CommMonoid.toMonoid
IsOrderedMonoid.toMulLeftMono
covariant_swap_mul_of_covariant_mul
CommMonoid.toCommSemigroup
WithBot
Monoid.toNatPow
Interval.commMonoid
map_pow
MonoidHom.instMonoidHomClass
coe_one_interval
coe_mul_interval
IsOrderedMonoid.toMulLeftMono
coe_sub_interval 📖mathematicalWithBot.some
NonemptyInterval
Preorder.toLE
instSubNonemptyInterval
WithBot
instSubInterval
coe_zero 📖mathematicalSetLike.coe
NonemptyInterval
Preorder.toLE
PartialOrder.toPreorder
setLike
instZeroNonemptyInterval
Set
Set.zero
coe_pure
coe_zero_interval 📖mathematicalWithBot.some
NonemptyInterval
Preorder.toLE
instZeroNonemptyInterval
WithBot
WithBot.zero
div_mem_div 📖mathematicalNonemptyInterval
Preorder.toLE
instMembership
instDivNonemptyInterval
DivInvMonoid.toDiv
Group.toDivInvMonoid
CommGroup.toGroup
div_le_div''
fst_add 📖mathematicaltoProd
Preorder.toLE
NonemptyInterval
instAddNonemptyInterval
fst_div 📖mathematicaltoProd
Preorder.toLE
NonemptyInterval
instDivNonemptyInterval
DivInvMonoid.toDiv
Group.toDivInvMonoid
CommGroup.toGroup
fst_inv 📖mathematicaltoProd
Preorder.toLE
PartialOrder.toPreorder
NonemptyInterval
instInvNonemptyInterval
InvOneClass.toInv
DivInvOneMonoid.toInvOneClass
DivisionMonoid.toDivInvOneMonoid
DivisionCommMonoid.toDivisionMonoid
CommGroup.toDivisionCommMonoid
fst_mul 📖mathematicaltoProd
Preorder.toLE
NonemptyInterval
instMulNonemptyInterval
fst_natCast 📖mathematicaltoProd
Preorder.toLE
NonemptyInterval
instNatCast
fst_neg 📖mathematicaltoProd
Preorder.toLE
PartialOrder.toPreorder
NonemptyInterval
instNegNonemptyInterval
NegZeroClass.toNeg
SubNegZeroMonoid.toNegZeroClass
SubtractionMonoid.toSubNegZeroMonoid
SubtractionCommMonoid.toSubtractionMonoid
AddCommGroup.toDivisionAddCommMonoid
fst_nsmul 📖mathematicaltoProd
Preorder.toLE
NonemptyInterval
hasNSMul
AddMonoid.toNatSMul
fst_one 📖mathematicaltoProd
Preorder.toLE
NonemptyInterval
instOneNonemptyInterval
fst_pow 📖mathematicaltoProd
Preorder.toLE
NonemptyInterval
hasPow
Monoid.toNatPow
fst_sub 📖mathematicaltoProd
Preorder.toLE
NonemptyInterval
instSubNonemptyInterval
fst_zero 📖mathematicaltoProd
Preorder.toLE
NonemptyInterval
instZeroNonemptyInterval
inv_mem_inv 📖mathematicalNonemptyInterval
Preorder.toLE
PartialOrder.toPreorder
instMembership
instInvNonemptyInterval
InvOneClass.toInv
DivInvOneMonoid.toInvOneClass
DivisionMonoid.toDivInvOneMonoid
DivisionCommMonoid.toDivisionMonoid
CommGroup.toDivisionCommMonoid
inv_le_inv'
inv_pure 📖mathematicalNonemptyInterval
Preorder.toLE
PartialOrder.toPreorder
instInvNonemptyInterval
pure
InvOneClass.toInv
DivInvOneMonoid.toInvOneClass
DivisionMonoid.toDivInvOneMonoid
DivisionCommMonoid.toDivisionMonoid
CommGroup.toDivisionCommMonoid
length_add 📖mathematicallength
NonemptyInterval
Preorder.toLE
PartialOrder.toPreorder
instAddNonemptyInterval
AddCommMagma.toAdd
AddCommSemigroup.toAddCommMagma
AddCommMonoid.toAddCommSemigroup
AddCommGroup.toAddCommMonoid
IsOrderedAddMonoid.toAddLeftMono
covariant_swap_add_of_covariant_add
add_sub_add_comm
length_neg 📖mathematicallength
NonemptyInterval
Preorder.toLE
PartialOrder.toPreorder
instNegNonemptyInterval
neg_sub_neg
length_nonneg 📖mathematicalPreorder.toLE
PartialOrder.toPreorder
NegZeroClass.toZero
SubNegZeroMonoid.toNegZeroClass
SubtractionMonoid.toSubNegZeroMonoid
SubtractionCommMonoid.toSubtractionMonoid
AddCommGroup.toDivisionAddCommMonoid
length
sub_nonneg_of_le
covariant_swap_add_of_covariant_add
IsOrderedAddMonoid.toAddLeftMono
fst_le_snd
length_pure 📖mathematicallength
pure
PartialOrder.toPreorder
NegZeroClass.toZero
SubNegZeroMonoid.toNegZeroClass
SubtractionMonoid.toSubNegZeroMonoid
SubtractionCommMonoid.toSubtractionMonoid
AddCommGroup.toDivisionAddCommMonoid
sub_self
length_sub 📖mathematicallength
NonemptyInterval
Preorder.toLE
PartialOrder.toPreorder
instSubNonemptyInterval
AddCommMonoid.toAddCommSemigroup
AddCommGroup.toAddCommMonoid
SubNegMonoid.toSub
AddGroup.toSubNegMonoid
AddCommGroup.toAddGroup
AddGroup.toOrderedSub
covariant_swap_add_of_covariant_add
IsOrderedAddMonoid.toAddLeftMono
AddCommMagma.toAdd
AddCommSemigroup.toAddCommMagma
AddGroup.toOrderedSub
covariant_swap_add_of_covariant_add
IsOrderedAddMonoid.toAddLeftMono
sub_eq_add_neg
length_add
length_neg
length_sum 📖mathematicallength
Finset.sum
NonemptyInterval
Preorder.toLE
PartialOrder.toPreorder
addCommMonoid
AddCommGroup.toAddCommMonoid
map_sum
AddMonoidHom.instAddMonoidHomClass
length_zero
length_add
length_zero 📖mathematicallength
NonemptyInterval
Preorder.toLE
PartialOrder.toPreorder
instZeroNonemptyInterval
NegZeroClass.toZero
SubNegZeroMonoid.toNegZeroClass
SubtractionMonoid.toSubNegZeroMonoid
SubtractionCommMonoid.toSubtractionMonoid
AddCommGroup.toDivisionAddCommMonoid
length_pure
mul_eq_one_iff 📖mathematicalNonemptyInterval
Preorder.toLE
PartialOrder.toPreorder
instMulNonemptyInterval
MulOne.toMul
MulOneClass.toMulOne
Monoid.toMulOneClass
DivInvMonoid.toMonoid
Group.toDivInvMonoid
CommGroup.toGroup
IsOrderedMonoid.toMulLeftMono
CommGroup.toCommMonoid
covariant_swap_mul_of_covariant_mul
CommMonoid.toCommSemigroup
instOneNonemptyInterval
InvOneClass.toOne
DivInvOneMonoid.toInvOneClass
DivisionMonoid.toDivInvOneMonoid
DivisionCommMonoid.toDivisionMonoid
CommGroup.toDivisionCommMonoid
pure
IsOrderedMonoid.toMulLeftMono
covariant_swap_mul_of_covariant_mul
mul_le_mul_iff_of_ge
IsLeftCancelMul.mulLeftStrictMono_of_mulLeftMono
LeftCancelSemigroup.toIsLeftCancelMul
IsRightCancelMul.mulRightStrictMono_of_mulRightMono
RightCancelSemigroup.toIsRightCancelMul
fst_le_snd
Eq.le
ext_iff
ext
pure_mul_pure
pure_one
neg_mem_neg 📖mathematicalNonemptyInterval
Preorder.toLE
PartialOrder.toPreorder
instMembership
instNegNonemptyInterval
NegZeroClass.toNeg
SubNegZeroMonoid.toNegZeroClass
SubtractionMonoid.toSubNegZeroMonoid
SubtractionCommMonoid.toSubtractionMonoid
AddCommGroup.toDivisionAddCommMonoid
neg_le_neg
neg_pure 📖mathematicalNonemptyInterval
Preorder.toLE
PartialOrder.toPreorder
instNegNonemptyInterval
pure
NegZeroClass.toNeg
SubNegZeroMonoid.toNegZeroClass
SubtractionMonoid.toSubNegZeroMonoid
SubtractionCommMonoid.toSubtractionMonoid
AddCommGroup.toDivisionAddCommMonoid
one_mem_one 📖mathematicalNonemptyInterval
Preorder.toLE
PartialOrder.toPreorder
instMembership
instOneNonemptyInterval
le_rfl
pure_add_pure 📖mathematicalNonemptyInterval
Preorder.toLE
instAddNonemptyInterval
pure
pure_div_pure 📖mathematicalNonemptyInterval
Preorder.toLE
instDivNonemptyInterval
pure
DivInvMonoid.toDiv
Group.toDivInvMonoid
CommGroup.toGroup
pure_mul_pure 📖mathematicalNonemptyInterval
Preorder.toLE
instMulNonemptyInterval
pure
pure_natCast 📖mathematicalpure
NonemptyInterval
Preorder.toLE
instNatCast
pure_nsmul 📖mathematicalNonemptyInterval
Preorder.toLE
hasNSMul
pure
AddMonoid.toNatSMul
pure_one 📖mathematicalpure
NonemptyInterval
Preorder.toLE
instOneNonemptyInterval
pure_pow 📖mathematicalNonemptyInterval
Preorder.toLE
hasPow
pure
Monoid.toNatPow
pure_sub_pure 📖mathematicalNonemptyInterval
Preorder.toLE
instSubNonemptyInterval
pure
pure_zero 📖mathematicalpure
NonemptyInterval
Preorder.toLE
instZeroNonemptyInterval
snd_add 📖mathematicaltoProd
Preorder.toLE
NonemptyInterval
instAddNonemptyInterval
snd_div 📖mathematicaltoProd
Preorder.toLE
NonemptyInterval
instDivNonemptyInterval
DivInvMonoid.toDiv
Group.toDivInvMonoid
CommGroup.toGroup
snd_inv 📖mathematicaltoProd
Preorder.toLE
PartialOrder.toPreorder
NonemptyInterval
instInvNonemptyInterval
InvOneClass.toInv
DivInvOneMonoid.toInvOneClass
DivisionMonoid.toDivInvOneMonoid
DivisionCommMonoid.toDivisionMonoid
CommGroup.toDivisionCommMonoid
snd_mul 📖mathematicaltoProd
Preorder.toLE
NonemptyInterval
instMulNonemptyInterval
snd_natCast 📖mathematicaltoProd
Preorder.toLE
NonemptyInterval
instNatCast
snd_neg 📖mathematicaltoProd
Preorder.toLE
PartialOrder.toPreorder
NonemptyInterval
instNegNonemptyInterval
NegZeroClass.toNeg
SubNegZeroMonoid.toNegZeroClass
SubtractionMonoid.toSubNegZeroMonoid
SubtractionCommMonoid.toSubtractionMonoid
AddCommGroup.toDivisionAddCommMonoid
snd_nsmul 📖mathematicaltoProd
Preorder.toLE
NonemptyInterval
hasNSMul
AddMonoid.toNatSMul
snd_one 📖mathematicaltoProd
Preorder.toLE
NonemptyInterval
instOneNonemptyInterval
snd_pow 📖mathematicaltoProd
Preorder.toLE
NonemptyInterval
hasPow
Monoid.toNatPow
snd_sub 📖mathematicaltoProd
Preorder.toLE
NonemptyInterval
instSubNonemptyInterval
snd_zero 📖mathematicaltoProd
Preorder.toLE
NonemptyInterval
instZeroNonemptyInterval
sub_mem_sub 📖mathematicalNonemptyInterval
Preorder.toLE
instMembership
instSubNonemptyIntervaltsub_le_tsub
toProd_add 📖mathematicaltoProd
Preorder.toLE
NonemptyInterval
instAddNonemptyInterval
Prod.instAdd
toProd_mul 📖mathematicaltoProd
Preorder.toLE
NonemptyInterval
instMulNonemptyInterval
Prod.instMul
toProd_nsmul 📖mathematicaltoProd
Preorder.toLE
NonemptyInterval
hasNSMul
Prod.instSMul
AddMonoid.toNatSMul
toProd_one 📖mathematicaltoProd
Preorder.toLE
NonemptyInterval
instOneNonemptyInterval
Prod.instOne
toProd_pow 📖mathematicaltoProd
Preorder.toLE
NonemptyInterval
hasPow
Prod.instPow
Monoid.toNatPow
toProd_zero 📖mathematicaltoProd
Preorder.toLE
NonemptyInterval
instZeroNonemptyInterval
Prod.instZero
zero_mem_zero 📖mathematicalNonemptyInterval
Preorder.toLE
PartialOrder.toPreorder
instMembership
instZeroNonemptyInterval
le_rfl

(root)

Definitions

NameCategoryTheorems
instAddInterval 📖CompOp
5 mathmath: Interval.bot_add, NonemptyInterval.coe_add_interval, Interval.add_eq_zero_iff, Interval.add_bot, Interval.length_add_le
instAddNonemptyInterval 📖CompOp
7 mathmath: NonemptyInterval.fst_add, NonemptyInterval.add_eq_zero_iff, NonemptyInterval.snd_add, NonemptyInterval.coe_add_interval, NonemptyInterval.pure_add_pure, NonemptyInterval.length_add, NonemptyInterval.toProd_add
instDivInterval 📖CompOp
3 mathmath: Interval.div_bot, NonemptyInterval.coe_div_interval, Interval.bot_div
instDivNonemptyInterval 📖CompOp
5 mathmath: NonemptyInterval.snd_div, NonemptyInterval.coe_div_interval, NonemptyInterval.fst_div, NonemptyInterval.pure_div_pure, NonemptyInterval.div_mem_div
instInvInterval 📖CompOp
2 mathmath: NonemptyInterval.coe_inv_interval, Interval.inv_bot
instInvNonemptyInterval 📖CompOp
5 mathmath: NonemptyInterval.coe_inv_interval, NonemptyInterval.snd_inv, NonemptyInterval.fst_inv, NonemptyInterval.inv_pure, NonemptyInterval.inv_mem_inv
instMulInterval 📖CompOp
4 mathmath: Interval.bot_mul, Interval.mul_bot, Interval.mul_eq_one_iff, NonemptyInterval.coe_mul_interval
instMulNonemptyInterval 📖CompOp
6 mathmath: NonemptyInterval.pure_mul_pure, NonemptyInterval.fst_mul, NonemptyInterval.toProd_mul, NonemptyInterval.snd_mul, NonemptyInterval.coe_mul_interval, NonemptyInterval.mul_eq_one_iff
instNegInterval 📖CompOp
3 mathmath: NonemptyInterval.coe_neg_interval, Interval.neg_bot, Interval.length_neg
instNegNonemptyInterval 📖CompOp
6 mathmath: NonemptyInterval.snd_neg, NonemptyInterval.coe_neg_interval, NonemptyInterval.fst_neg, NonemptyInterval.neg_pure, NonemptyInterval.neg_mem_neg, NonemptyInterval.length_neg
instOneNonemptyInterval 📖CompOp
12 mathmath: NonemptyInterval.coe_one_interval, NonemptyInterval.toProd_one, Interval.one_mem_one, NonemptyInterval.coe_one, NonemptyInterval.one_mem_one, NonemptyInterval.snd_one, Interval.coe_one, NonemptyInterval.fst_one, NonemptyInterval.pure_one, Interval.pure_one, Interval.mul_eq_one_iff, NonemptyInterval.mul_eq_one_iff
instSubInterval 📖CompOp
4 mathmath: Interval.length_sub_le, NonemptyInterval.coe_sub_interval, Interval.sub_bot, Interval.bot_sub
instSubNonemptyInterval 📖CompOp
6 mathmath: NonemptyInterval.coe_sub_interval, NonemptyInterval.fst_sub, NonemptyInterval.pure_sub_pure, NonemptyInterval.snd_sub, NonemptyInterval.sub_mem_sub, NonemptyInterval.length_sub
instZeroNonemptyInterval 📖CompOp
14 mathmath: NonemptyInterval.length_zero, NonemptyInterval.snd_zero, NonemptyInterval.add_eq_zero_iff, NonemptyInterval.coe_zero, Interval.coe_zero, NonemptyInterval.toProd_zero, Interval.pure_zero, Interval.add_eq_zero_iff, NonemptyInterval.fst_zero, Interval.length_zero, NonemptyInterval.coe_zero_interval, NonemptyInterval.zero_mem_zero, Interval.zero_mem_zero, NonemptyInterval.pure_zero

---

← Back to Index