Group

📁 Source: Mathlib/Algebra/Order/Interval/Set/Group.lean

Statistics

Metric	Count
Definitions	0
Theorems add_mem_Icc_iff_left, add_mem_Icc_iff_right, add_mem_Ico_iff_left, add_mem_Ico_iff_right, add_mem_Ioc_iff_left, add_mem_Ioc_iff_right, add_mem_Ioo_iff_left, add_mem_Ioo_iff_right, inv_mem_Icc_iff, inv_mem_Ico_iff, inv_mem_Ioc_iff, inv_mem_Ioo_iff, mem_Icc_iff_abs_le, neg_mem_Icc_iff, neg_mem_Ico_iff, neg_mem_Ioc_iff, neg_mem_Ioo_iff, nonempty_Ico_sdiff, pairwise_disjoint_Ico_add_intCast, pairwise_disjoint_Ico_add_zsmul, pairwise_disjoint_Ico_intCast, pairwise_disjoint_Ico_mul_zpow, pairwise_disjoint_Ico_zpow, pairwise_disjoint_Ico_zsmul, pairwise_disjoint_Ioc_add_intCast, pairwise_disjoint_Ioc_add_zsmul, pairwise_disjoint_Ioc_intCast, pairwise_disjoint_Ioc_mul_zpow, pairwise_disjoint_Ioc_zpow, pairwise_disjoint_Ioc_zsmul, pairwise_disjoint_Ioo_add_intCast, pairwise_disjoint_Ioo_add_zsmul, pairwise_disjoint_Ioo_intCast, pairwise_disjoint_Ioo_mul_zpow, pairwise_disjoint_Ioo_zpow, pairwise_disjoint_Ioo_zsmul, sub_mem_Icc_iff_left, sub_mem_Icc_iff_right, sub_mem_Icc_zero_iff_right, sub_mem_Ico_iff_left, sub_mem_Ico_iff_right, sub_mem_Ico_zero_iff_right, sub_mem_Ioc_iff_left, sub_mem_Ioc_iff_right, sub_mem_Ioc_zero_iff_right, sub_mem_Ioo_iff_left, sub_mem_Ioo_iff_right, sub_mem_Ioo_zero_iff_right	48
Total	48

Set

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_mem_Icc_iff_left 📖	mathematical	—	Set instMembership Icc PartialOrder.toPreorder AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	sub_le_iff_le_add covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono le_sub_iff_add_le
add_mem_Icc_iff_right 📖	mathematical	—	Set instMembership Icc PartialOrder.toPreorder AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	sub_le_iff_le_add' IsOrderedAddMonoid.toAddLeftMono le_sub_iff_add_le'
add_mem_Ico_iff_left 📖	mathematical	—	Set instMembership Ico PartialOrder.toPreorder AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	sub_le_iff_le_add covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono lt_sub_iff_add_lt IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd
add_mem_Ico_iff_right 📖	mathematical	—	Set instMembership Ico PartialOrder.toPreorder AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	sub_le_iff_le_add' IsOrderedAddMonoid.toAddLeftMono lt_sub_iff_add_lt' IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd
add_mem_Ioc_iff_left 📖	mathematical	—	Set instMembership Ioc PartialOrder.toPreorder AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	sub_lt_iff_lt_add IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono le_sub_iff_add_le
add_mem_Ioc_iff_right 📖	mathematical	—	Set instMembership Ioc PartialOrder.toPreorder AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	sub_lt_iff_lt_add' IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono le_sub_iff_add_le'
add_mem_Ioo_iff_left 📖	mathematical	—	Set instMembership Ioo PartialOrder.toPreorder AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	sub_lt_iff_lt_add IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono lt_sub_iff_add_lt
add_mem_Ioo_iff_right 📖	mathematical	—	Set instMembership Ioo PartialOrder.toPreorder AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	sub_lt_iff_lt_add' IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono lt_sub_iff_add_lt'
inv_mem_Icc_iff 📖	mathematical	—	Set instMembership Icc PartialOrder.toPreorder InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroup.toDivisionCommMonoid	—	inv_le' IsOrderedMonoid.toMulLeftMono covariant_swap_mul_of_covariant_mul le_inv'
inv_mem_Ico_iff 📖	mathematical	—	Set instMembership Ico PartialOrder.toPreorder InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroup.toDivisionCommMonoid Ioc	—	inv_lt' IsLeftCancelMul.mulLeftStrictMono_of_mulLeftMono LeftCancelSemigroup.toIsLeftCancelMul IsOrderedMonoid.toMulLeftMono IsRightCancelMul.mulRightStrictMono_of_mulRightMono RightCancelSemigroup.toIsRightCancelMul covariant_swap_mul_of_covariant_mul le_inv'
inv_mem_Ioc_iff 📖	mathematical	—	Set instMembership Ioc PartialOrder.toPreorder InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroup.toDivisionCommMonoid Ico	—	inv_le' IsOrderedMonoid.toMulLeftMono covariant_swap_mul_of_covariant_mul lt_inv' IsLeftCancelMul.mulLeftStrictMono_of_mulLeftMono LeftCancelSemigroup.toIsLeftCancelMul IsRightCancelMul.mulRightStrictMono_of_mulRightMono RightCancelSemigroup.toIsRightCancelMul
inv_mem_Ioo_iff 📖	mathematical	—	Set instMembership Ioo PartialOrder.toPreorder InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroup.toDivisionCommMonoid	—	inv_lt' IsLeftCancelMul.mulLeftStrictMono_of_mulLeftMono LeftCancelSemigroup.toIsLeftCancelMul IsOrderedMonoid.toMulLeftMono IsRightCancelMul.mulRightStrictMono_of_mulRightMono RightCancelSemigroup.toIsRightCancelMul covariant_swap_mul_of_covariant_mul lt_inv'
mem_Icc_iff_abs_le 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder abs AddCommGroup.toAddGroup SubNegMonoid.toSub AddGroup.toSubNegMonoid Set instMembership Icc AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid	—	abs_le sub_le_comm IsOrderedAddMonoid.toAddLeftMono neg_le_sub_iff_le_add
neg_mem_Icc_iff 📖	mathematical	—	Set instMembership Icc PartialOrder.toPreorder NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	neg_le IsOrderedAddMonoid.toAddLeftMono covariant_swap_add_of_covariant_add le_neg
neg_mem_Ico_iff 📖	mathematical	—	Set instMembership Ico PartialOrder.toPreorder NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ioc	—	neg_lt IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add le_neg
neg_mem_Ioc_iff 📖	mathematical	—	Set instMembership Ioc PartialOrder.toPreorder NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ico	—	neg_le IsOrderedAddMonoid.toAddLeftMono covariant_swap_add_of_covariant_add lt_neg IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd
neg_mem_Ioo_iff 📖	mathematical	—	Set instMembership Ioo PartialOrder.toPreorder NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	neg_lt IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add lt_neg
nonempty_Ico_sdiff 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	Elem Set instSDiff Ico AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid	—	lt_or_ge IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono contravariant_lt_of_covariant_le not_le IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add contravariant_swap_add_of_contravariant_add
pairwise_disjoint_Ico_add_intCast 📖	mathematical	—	Pairwise Function.onFun Set Disjoint SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra BiheytingAlgebra.toCoheytingAlgebra BooleanAlgebra.toBiheytingAlgebra instBooleanAlgebra HeytingAlgebra.toOrderBot BiheytingAlgebra.toHeytingAlgebra Ico PartialOrder.toPreorder Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing AddGroupWithOne.toIntCast Ring.toAddGroupWithOne AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne	—	zsmul_one Int.cast_add Int.cast_one pairwise_disjoint_Ico_add_zsmul IsOrderedRing.toIsOrderedAddMonoid
pairwise_disjoint_Ico_add_zsmul 📖	mathematical	—	Pairwise Function.onFun Set Disjoint SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra BiheytingAlgebra.toCoheytingAlgebra BooleanAlgebra.toBiheytingAlgebra instBooleanAlgebra HeytingAlgebra.toOrderBot BiheytingAlgebra.toHeytingAlgebra Ico PartialOrder.toPreorder AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup SubNegMonoid.toZSMul	—	disjoint_iff LE.le.trans_lt add_lt_add_iff_left IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono IsOrderedCancelAddMonoid.toAddLeftReflectLT IsOrderedAddMonoid.toIsOrderedCancelAddMonoid add_one_zsmul add_zero le_antisymm zsmul_lt_zsmul_iff_left
pairwise_disjoint_Ico_intCast 📖	mathematical	—	Pairwise Function.onFun Set Disjoint SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra BiheytingAlgebra.toCoheytingAlgebra BooleanAlgebra.toBiheytingAlgebra instBooleanAlgebra HeytingAlgebra.toOrderBot BiheytingAlgebra.toHeytingAlgebra Ico PartialOrder.toPreorder AddGroupWithOne.toIntCast Ring.toAddGroupWithOne Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne	—	zero_add pairwise_disjoint_Ico_add_intCast
pairwise_disjoint_Ico_mul_zpow 📖	mathematical	—	Pairwise Function.onFun Set Disjoint SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra BiheytingAlgebra.toCoheytingAlgebra BooleanAlgebra.toBiheytingAlgebra instBooleanAlgebra HeytingAlgebra.toOrderBot BiheytingAlgebra.toHeytingAlgebra Ico PartialOrder.toPreorder MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup DivInvMonoid.toZPow	—	LE.le.trans_lt mul_lt_mul_iff_left IsLeftCancelMul.mulLeftStrictMono_of_mulLeftMono LeftCancelSemigroup.toIsLeftCancelMul IsOrderedMonoid.toMulLeftMono IsOrderedCancelMonoid.toMulLeftReflectLT IsOrderedMonoid.toIsOrderedCancelMonoid zpow_add_one mul_one le_antisymm zpow_lt_zpow_iff_right
pairwise_disjoint_Ico_zpow 📖	mathematical	—	Pairwise Function.onFun Set Disjoint SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra BiheytingAlgebra.toCoheytingAlgebra BooleanAlgebra.toBiheytingAlgebra instBooleanAlgebra HeytingAlgebra.toOrderBot BiheytingAlgebra.toHeytingAlgebra Ico PartialOrder.toPreorder DivInvMonoid.toZPow Group.toDivInvMonoid CommGroup.toGroup	—	one_mul pairwise_disjoint_Ico_mul_zpow
pairwise_disjoint_Ico_zsmul 📖	mathematical	—	Pairwise Function.onFun Set Disjoint SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra BiheytingAlgebra.toCoheytingAlgebra BooleanAlgebra.toBiheytingAlgebra instBooleanAlgebra HeytingAlgebra.toOrderBot BiheytingAlgebra.toHeytingAlgebra Ico PartialOrder.toPreorder SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	zero_add pairwise_disjoint_Ico_add_zsmul
pairwise_disjoint_Ioc_add_intCast 📖	mathematical	—	Pairwise Function.onFun Set Disjoint SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra BiheytingAlgebra.toCoheytingAlgebra BooleanAlgebra.toBiheytingAlgebra instBooleanAlgebra HeytingAlgebra.toOrderBot BiheytingAlgebra.toHeytingAlgebra Ioc PartialOrder.toPreorder Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing AddGroupWithOne.toIntCast Ring.toAddGroupWithOne AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne	—	zsmul_one Int.cast_add Int.cast_one pairwise_disjoint_Ioc_add_zsmul IsOrderedRing.toIsOrderedAddMonoid
pairwise_disjoint_Ioc_add_zsmul 📖	mathematical	—	Pairwise Function.onFun Set Disjoint SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra BiheytingAlgebra.toCoheytingAlgebra BooleanAlgebra.toBiheytingAlgebra instBooleanAlgebra HeytingAlgebra.toOrderBot BiheytingAlgebra.toHeytingAlgebra Ioc PartialOrder.toPreorder AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup SubNegMonoid.toZSMul	—	disjoint_iff LT.lt.trans_le add_lt_add_iff_left IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono IsOrderedCancelAddMonoid.toAddLeftReflectLT IsOrderedAddMonoid.toIsOrderedCancelAddMonoid add_one_zsmul add_zero le_antisymm zsmul_lt_zsmul_iff_left
pairwise_disjoint_Ioc_intCast 📖	mathematical	—	Pairwise Function.onFun Set Disjoint SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra BiheytingAlgebra.toCoheytingAlgebra BooleanAlgebra.toBiheytingAlgebra instBooleanAlgebra HeytingAlgebra.toOrderBot BiheytingAlgebra.toHeytingAlgebra Ioc PartialOrder.toPreorder AddGroupWithOne.toIntCast Ring.toAddGroupWithOne Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne	—	zero_add pairwise_disjoint_Ioc_add_intCast
pairwise_disjoint_Ioc_mul_zpow 📖	mathematical	—	Pairwise Function.onFun Set Disjoint SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra BiheytingAlgebra.toCoheytingAlgebra BooleanAlgebra.toBiheytingAlgebra instBooleanAlgebra HeytingAlgebra.toOrderBot BiheytingAlgebra.toHeytingAlgebra Ioc PartialOrder.toPreorder MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup DivInvMonoid.toZPow	—	LT.lt.trans_le mul_lt_mul_iff_left IsLeftCancelMul.mulLeftStrictMono_of_mulLeftMono LeftCancelSemigroup.toIsLeftCancelMul IsOrderedMonoid.toMulLeftMono IsOrderedCancelMonoid.toMulLeftReflectLT IsOrderedMonoid.toIsOrderedCancelMonoid zpow_add_one mul_one le_antisymm zpow_lt_zpow_iff_right
pairwise_disjoint_Ioc_zpow 📖	mathematical	—	Pairwise Function.onFun Set Disjoint SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra BiheytingAlgebra.toCoheytingAlgebra BooleanAlgebra.toBiheytingAlgebra instBooleanAlgebra HeytingAlgebra.toOrderBot BiheytingAlgebra.toHeytingAlgebra Ioc PartialOrder.toPreorder DivInvMonoid.toZPow Group.toDivInvMonoid CommGroup.toGroup	—	one_mul pairwise_disjoint_Ioc_mul_zpow
pairwise_disjoint_Ioc_zsmul 📖	mathematical	—	Pairwise Function.onFun Set Disjoint SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra BiheytingAlgebra.toCoheytingAlgebra BooleanAlgebra.toBiheytingAlgebra instBooleanAlgebra HeytingAlgebra.toOrderBot BiheytingAlgebra.toHeytingAlgebra Ioc PartialOrder.toPreorder SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	zero_add pairwise_disjoint_Ioc_add_zsmul
pairwise_disjoint_Ioo_add_intCast 📖	mathematical	—	Pairwise Function.onFun Set Disjoint SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra BiheytingAlgebra.toCoheytingAlgebra BooleanAlgebra.toBiheytingAlgebra instBooleanAlgebra HeytingAlgebra.toOrderBot BiheytingAlgebra.toHeytingAlgebra Ioo PartialOrder.toPreorder Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing AddGroupWithOne.toIntCast Ring.toAddGroupWithOne AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne	—	zsmul_one Int.cast_add Int.cast_one pairwise_disjoint_Ioo_add_zsmul IsOrderedRing.toIsOrderedAddMonoid
pairwise_disjoint_Ioo_add_zsmul 📖	mathematical	—	Pairwise Function.onFun Set Disjoint SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra BiheytingAlgebra.toCoheytingAlgebra BooleanAlgebra.toBiheytingAlgebra instBooleanAlgebra HeytingAlgebra.toOrderBot BiheytingAlgebra.toHeytingAlgebra Ioo PartialOrder.toPreorder AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup SubNegMonoid.toZSMul	—	Disjoint.mono Ioo_subset_Ioc_self pairwise_disjoint_Ioc_add_zsmul
pairwise_disjoint_Ioo_intCast 📖	mathematical	—	Pairwise Function.onFun Set Disjoint SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra BiheytingAlgebra.toCoheytingAlgebra BooleanAlgebra.toBiheytingAlgebra instBooleanAlgebra HeytingAlgebra.toOrderBot BiheytingAlgebra.toHeytingAlgebra Ioo PartialOrder.toPreorder AddGroupWithOne.toIntCast Ring.toAddGroupWithOne Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne	—	zero_add pairwise_disjoint_Ioo_add_intCast
pairwise_disjoint_Ioo_mul_zpow 📖	mathematical	—	Pairwise Function.onFun Set Disjoint SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra BiheytingAlgebra.toCoheytingAlgebra BooleanAlgebra.toBiheytingAlgebra instBooleanAlgebra HeytingAlgebra.toOrderBot BiheytingAlgebra.toHeytingAlgebra Ioo PartialOrder.toPreorder MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup DivInvMonoid.toZPow	—	Disjoint.mono Ioo_subset_Ioc_self pairwise_disjoint_Ioc_mul_zpow
pairwise_disjoint_Ioo_zpow 📖	mathematical	—	Pairwise Function.onFun Set Disjoint SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra BiheytingAlgebra.toCoheytingAlgebra BooleanAlgebra.toBiheytingAlgebra instBooleanAlgebra HeytingAlgebra.toOrderBot BiheytingAlgebra.toHeytingAlgebra Ioo PartialOrder.toPreorder DivInvMonoid.toZPow Group.toDivInvMonoid CommGroup.toGroup	—	one_mul pairwise_disjoint_Ioo_mul_zpow
pairwise_disjoint_Ioo_zsmul 📖	mathematical	—	Pairwise Function.onFun Set Disjoint SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra BiheytingAlgebra.toCoheytingAlgebra BooleanAlgebra.toBiheytingAlgebra instBooleanAlgebra HeytingAlgebra.toOrderBot BiheytingAlgebra.toHeytingAlgebra Ioo PartialOrder.toPreorder SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	zero_add pairwise_disjoint_Ioo_add_zsmul
sub_mem_Icc_iff_left 📖	mathematical	—	Set instMembership Icc PartialOrder.toPreorder SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid	—	le_sub_iff_add_le covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono sub_le_iff_le_add
sub_mem_Icc_iff_right 📖	mathematical	—	Set instMembership Icc PartialOrder.toPreorder SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	sub_le_comm IsOrderedAddMonoid.toAddLeftMono le_sub_comm
sub_mem_Icc_zero_iff_right 📖	mathematical	—	Set instMembership Icc PartialOrder.toPreorder NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	sub_self sub_zero
sub_mem_Ico_iff_left 📖	mathematical	—	Set instMembership Ico PartialOrder.toPreorder SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid	—	le_sub_iff_add_le covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono sub_lt_iff_lt_add IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd
sub_mem_Ico_iff_right 📖	mathematical	—	Set instMembership Ico PartialOrder.toPreorder SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Ioc	—	sub_lt_comm IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono le_sub_comm
sub_mem_Ico_zero_iff_right 📖	mathematical	—	Set instMembership Ico PartialOrder.toPreorder NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Ioc	—	sub_self sub_zero
sub_mem_Ioc_iff_left 📖	mathematical	—	Set instMembership Ioc PartialOrder.toPreorder SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid	—	lt_sub_iff_add_lt IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono sub_le_iff_le_add
sub_mem_Ioc_iff_right 📖	mathematical	—	Set instMembership Ioc PartialOrder.toPreorder SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Ico	—	sub_le_comm IsOrderedAddMonoid.toAddLeftMono lt_sub_comm IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd
sub_mem_Ioc_zero_iff_right 📖	mathematical	—	Set instMembership Ioc PartialOrder.toPreorder NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Ico	—	sub_self sub_zero
sub_mem_Ioo_iff_left 📖	mathematical	—	Set instMembership Ioo PartialOrder.toPreorder SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid	—	lt_sub_iff_add_lt IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono sub_lt_iff_lt_add
sub_mem_Ioo_iff_right 📖	mathematical	—	Set instMembership Ioo PartialOrder.toPreorder SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	sub_lt_comm IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono lt_sub_comm
sub_mem_Ioo_zero_iff_right 📖	mathematical	—	Set instMembership Ioo PartialOrder.toPreorder NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	sub_self sub_zero

---

← Back to Index