Instances

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

Statistics

Metric	Count
Definitions instCommMonoidWithZero, instMonoidWithZero, instMul, instOne, instPow, instZero, instCommSemigroup, instMul, instSemigroup, instZero, instCancelCommMonoid, instCancelMonoid, instCommMonoid, instCommSemigroup, instMonoid, instMul, instOne, instPow, instSemigroup, instCommSemigroup, instMul, instSemigroup	22
Theorems coe_eq_one, coe_eq_zero, coe_le_one, coe_mul, coe_ne_one, coe_ne_zero, coe_nonneg, coe_one, coe_pow, coe_zero, instIsCancelMulZero, instZeroLEOneClass, le_one, mem_iff_one_sub_mem, mk_one, mk_zero, mul_le_left, mul_le_right, nonneg, one_sub_le_one, one_sub_mem, one_sub_nonneg, coe_eq_zero, coe_lt_one, coe_mul, coe_ne_zero, coe_nonneg, coe_zero, mk_zero, nonneg, coe_eq_one, coe_le_one, coe_mul, coe_ne_one, coe_one, coe_pos, coe_pow, le_one, mk_one, coe_mul, lt_one, mem_iff_one_sub_mem, one_minus_lt_one, one_minus_pos, one_sub_mem, pos	46
Total	68

Set.Icc

Definitions

Name	Category	Theorems
instCommMonoidWithZero 📖	CompOp	—
instMonoidWithZero 📖	CompOp	—
instMul 📖	CompOp	6 math math: coe_mul, unitInterval.mul_le_left, unitInterval.mul_le_right, instIsCancelMulZero, mul_le_left, mul_le_right
instOne 📖	CompOp	62 math math: completelyRegularSpace_iff_isOpen, IsCoveringMap.liftPath_apply_one_eq_of_homotopicRel, ContinuousMap.Homotopy.curveIntegral_add_curveIntegral_eq_of_hasFDerivWithinAt, ContinuousMap.Homotopy.evalAt_eq, Path.Homotopy.target, ContinuousMap.HomotopyWith.apply_one, unitInterval.qRight_one_left, Path.delayReflLeft_one, ProbabilityTheory.setBernoulli_one, ContinuousMap.Homotopy.curveIntegral_add_curveIntegral_eq_of_hasFDerivWithinAt_off_countable, Path.subpathAux_one, unitInterval.lt_one_iff_ne_one, convexCombo_one, ContinuousMap.Homotopy.apply_one_path, projIcc_eq_one, Path.Homotopy.transAssocReparamAux_one, Path.Homotopy.transReflReparamAux_one, unitInterval.range_sigmoid, Path.reparam_id, Path.Homotopy.trans_assoc_reparam, unitInterval.symm_one, exists_monotone_Icc_subset_open_cover_unitInterval_prod_self, unitInterval.le_one', le_one, bernsteinApproximation.apply_one, unitInterval.symm_eq_zero, CompletelyRegularSpace.completely_regular, ContinuousMap.HomotopyLike.map_one_left, unitInterval.tendsto_sigmoid_atTop, unitInterval.symm_zero, mk_one, unitInterval.subtype_Ici_eq_Icc, unitInterval.coe_lt_one, Path.target', coe_one, stdSimplexHomeomorphUnitInterval_one, Path.range_coe, ContinuousMap.Homotopy.curveIntegral_add_curveIntegral_eq_of_diffContOnCl, Path.id_apply, ContinuousMap.Homotopy.map_one_left, ContinuousMap.Homotopy.apply_one, Path.Homotopy.trans_refl_reparam, coe_eq_one, exists_monotone_Icc_subset_open_cover_unitInterval, Path.delayReflRight_one, Path.Homotopy.eval_one, Path.target, bernstein.z_last, completelyRegularSpace_iff, unitInterval.univ_eq_Icc, unitInterval.eq_one_or_eq_zero_of_le_mul, Path.subpath_zero_one, ContinuousMap.Homotopy.curry_one, unitInterval.subtype_Ioi_eq_Ioc, stdSimplexEquivIcc_one, unitInterval.symm_eq_one, unitInterval.sigmoid_lt_one, unitInterval.qRight_one_right, unitInterval.toNNReal_one, CompletelyRegularSpace.completely_regular_isOpen, instZeroLEOneClass, IsCoveringMap.liftPath_trans
instPow 📖	CompOp	1 math math: coe_pow
instZero 📖	CompOp	64 math math: completelyRegularSpace_iff_isOpen, bernsteinApproximation.apply_zero, ProbabilityTheory.unitInterval.cdf_eq_real, coe_zero, ContinuousMap.Homotopy.curveIntegral_add_curveIntegral_eq_of_hasFDerivWithinAt, ContinuousMap.Homotopy.apply_zero_path, unitInterval.pos_iff_ne_zero, ContinuousMap.HomotopyLike.map_zero_left, ContinuousMap.Homotopy.evalAt_eq, nonneg, stdSimplexHomeomorphUnitInterval_zero, Path.delayReflRight_zero, Path.Homotopy.eval_zero, ContinuousMap.Homotopy.curveIntegral_add_curveIntegral_eq_of_hasFDerivWithinAt_off_countable, unitInterval.toNNReal_zero, mk_zero, Path.Homotopy.transAssocReparamAux_zero, unitInterval.range_sigmoid, Path.source', Path.reparam_id, Path.Homotopy.trans_assoc_reparam, unitInterval.symm_one, Path.delayReflLeft_zero, unitInterval.qRight_zero_right, exists_monotone_Icc_subset_open_cover_unitInterval_prod_self, instIsCancelMulZero, unitInterval.nonneg', ProbabilityTheory.setBernoulli_zero, unitInterval.qRight_zero_left, unitInterval.symm_eq_zero, Path.Homotopy.transReflReparamAux_zero, coe_eq_zero, bernstein.z_zero, CompletelyRegularSpace.completely_regular, unitInterval.symm_zero, unitInterval.subtype_Iio_eq_Ico, unitInterval.coe_pos, Path.range_coe, ContinuousMap.Homotopy.apply_zero, ContinuousMap.Homotopy.curveIntegral_add_curveIntegral_eq_of_diffContOnCl, Path.id_apply, Path.source, Path.Homotopy.trans_refl_reparam, exists_monotone_Icc_subset_open_cover_unitInterval, Path.subpathAux_zero, Path.Homotopy.source, completelyRegularSpace_iff, unitInterval.univ_eq_Icc, unitInterval.subtype_Iic_eq_Icc, ContinuousMap.HomotopyWith.apply_zero, projIcc_eq_zero, unitInterval.eq_one_or_eq_zero_of_le_mul, unitInterval.sigmoid_pos, Path.subpath_zero_one, ContDiffPointwiseHolderAt.zero_exponent_iff, unitInterval.tendsto_sigmoid_atBot, unitInterval.symm_eq_one, ContinuousMap.Homotopy.map_zero_left, CompletelyRegularSpace.completely_regular_isOpen, convexCombo_zero, ContinuousMap.Homotopy.curry_zero, stdSimplexEquivIcc_zero, instZeroLEOneClass, IsCoveringMap.liftPath_trans

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_eq_one 📖	mathematical	—	Set Set.instMembership Set.Icc PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Set.Elem instOne	—	—
coe_eq_zero 📖	mathematical	—	Set Set.instMembership Set.Icc PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Set.Elem instZero	—	—
coe_le_one 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder Set Set.instMembership Set.Icc MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	—
coe_mul 📖	mathematical	—	Set Set.instMembership Set.Icc PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Set.Elem instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	—
coe_ne_one 📖	—	—	—	—	not_iff_not coe_eq_one
coe_ne_zero 📖	—	—	—	—	not_iff_not coe_eq_zero
coe_nonneg 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Set Set.instMembership Set.Icc AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	—
coe_one 📖	mathematical	—	Set Set.instMembership Set.Icc PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Set.Elem instOne	—	—
coe_pow 📖	mathematical	—	Set Set.instMembership Set.Icc PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Set.Elem instPow Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	—
coe_zero 📖	mathematical	—	Set Set.instMembership Set.Icc PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Set.Elem instZero	—	—
instIsCancelMulZero 📖	mathematical	—	IsCancelMulZero Set.Elem Set.Icc PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne instMul Ring.toSemiring instZero	—	Function.Injective.isCancelMulZero Subtype.coe_injective coe_zero coe_mul NoZeroDivisors.toIsCancelMulZero
instZeroLEOneClass 📖	mathematical	—	ZeroLEOneClass Set.Elem Set.Icc PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne instZero instOne Preorder.toLE Set Set.instMembership	—	Subtype.coe_le_coe zero_le_one IsOrderedRing.toZeroLEOneClass
le_one 📖	mathematical	—	Set.Elem Set.Icc PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Preorder.toLE Set Set.instMembership instOne	—	—
mem_iff_one_sub_mem 📖	mathematical	—	Set Set.instMembership Set.Icc PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup	—	one_sub_mem sub_sub_cancel
mk_one 📖	mathematical	Set Set.instMembership Set.Icc PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	instOne	—	—
mk_zero 📖	mathematical	Set Set.instMembership Set.Icc PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	instZero	—	—
mul_le_left 📖	mathematical	—	Set.Elem Set.Icc PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Preorder.toLE Set Set.instMembership instMul	—	LE.le.trans_eq mul_le_mul_of_nonneg_left IsOrderedRing.toPosMulMono mul_one
mul_le_right 📖	mathematical	—	Set.Elem Set.Icc PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Preorder.toLE Set Set.instMembership instMul	—	LE.le.trans_eq mul_le_mul_of_nonneg_right IsOrderedRing.toMulPosMono one_mul
nonneg 📖	mathematical	—	Set.Elem Set.Icc PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Preorder.toLE Set Set.instMembership instZero	—	—
one_sub_le_one 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Set Set.instMembership Set.Icc MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	AddGroup.toOrderedSub covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedCancelAddMonoid.toAddLeftReflectLT IsOrderedAddMonoid.toIsOrderedCancelAddMonoid
one_sub_mem 📖	mathematical	Set Set.instMembership Set.Icc PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup	—	Set.mem_Icc sub_nonneg covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid sub_le_self_iff
one_sub_nonneg 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Set Set.instMembership Set.Icc	—	covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid

Set.Ico

Definitions

Name	Category	Theorems
instCommSemigroup 📖	CompOp	—
instMul 📖	CompOp	1 math math: coe_mul
instSemigroup 📖	CompOp	—
instZero 📖	CompOp	4 math math: coe_zero, nonneg, coe_eq_zero, mk_zero

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_eq_zero 📖	mathematical	—	Set Set.instMembership Set.Ico PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Set.Elem instZero	—	—
coe_lt_one 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder Set Set.instMembership Set.Ico MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	—
coe_mul 📖	mathematical	—	Set Set.instMembership Set.Ico PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Set.Elem instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	—
coe_ne_zero 📖	—	—	—	—	not_iff_not coe_eq_zero
coe_nonneg 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Set Set.instMembership Set.Ico AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	—
coe_zero 📖	mathematical	—	Set Set.instMembership Set.Ico PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Set.Elem instZero	—	—
mk_zero 📖	mathematical	Set Set.instMembership Set.Ico PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	instZero	—	—
nonneg 📖	mathematical	—	Set.Elem Set.Ico PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Preorder.toLE Set Set.instMembership instZero	—	—

Set.Ioc

Definitions

Name	Category	Theorems
instCancelCommMonoid 📖	CompOp	—
instCancelMonoid 📖	CompOp	—
instCommMonoid 📖	CompOp	—
instCommSemigroup 📖	CompOp	—
instMonoid 📖	CompOp	—
instMul 📖	CompOp	1 math math: coe_mul
instOne 📖	CompOp	4 math math: mk_one, coe_eq_one, coe_one, le_one
instPow 📖	CompOp	1 math math: coe_pow
instSemigroup 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_eq_one 📖	mathematical	—	Set Set.instMembership Set.Ioc PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Set.Elem instOne	—	—
coe_le_one 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder Set Set.instMembership Set.Ioc MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	—
coe_mul 📖	mathematical	—	Set Set.instMembership Set.Ioc PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Set.Elem instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	—
coe_ne_one 📖	—	—	—	—	not_iff_not coe_eq_one
coe_one 📖	mathematical	—	Set Set.instMembership Set.Ioc PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Set.Elem instOne	—	—
coe_pos 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Set Set.instMembership Set.Ioc AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	—
coe_pow 📖	mathematical	—	Set Set.instMembership Set.Ioc PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Set.Elem instPow Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	—
le_one 📖	mathematical	—	Set.Elem Set.Ioc PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Preorder.toLE Set Set.instMembership instOne	—	—
mk_one 📖	mathematical	Set Set.instMembership Set.Ioc PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	instOne	—	—

Set.Ioo

Definitions

Name	Category	Theorems
instCommSemigroup 📖	CompOp	—
instMul 📖	CompOp	1 math math: coe_mul
instSemigroup 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_mul 📖	mathematical	—	Set Set.instMembership Set.Ioo PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Set.Elem instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	—
lt_one 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder Set Set.instMembership Set.Ioo MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	—
mem_iff_one_sub_mem 📖	mathematical	—	Set Set.instMembership Set.Ioo PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup	—	one_sub_mem sub_sub_cancel
one_minus_lt_one 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Set Set.instMembership Set.Ioo MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid
one_minus_pos 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Set Set.instMembership Set.Ioo	—	IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid
one_sub_mem 📖	mathematical	Set Set.instMembership Set.Ioo PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup	—	IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd
pos 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Set Set.instMembership Set.Ioo AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	—

---

← Back to Index