Pointwise

📁 Source: Mathlib/Data/Real/Pointwise.lean

Statistics

Metric	Count
Definitions	0
Theorems iInf_mul_of_nonneg, iInf_mul_of_nonpos, iSup_mul_of_nonneg, iSup_mul_of_nonpos, mul_iInf_of_nonneg, mul_iInf_of_nonpos, mul_iSup_of_nonneg, mul_iSup_of_nonpos, sInf_smul_of_nonneg, sInf_smul_of_nonpos, sSup_smul_of_nonneg, sSup_smul_of_nonpos, smul_iInf_of_nonneg, smul_iInf_of_nonpos, smul_iSup_of_nonneg, smul_iSup_of_nonpos	16
Total	16

Real

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
iInf_mul_of_nonneg 📖	mathematical	Real instLE instZero	Real instMul iInf instInfSet	—	mul_comm mul_iInf_of_nonneg
iInf_mul_of_nonpos 📖	mathematical	Real instLE instZero	Real instMul iInf instInfSet iSup instSupSet	—	mul_comm mul_iInf_of_nonpos
iSup_mul_of_nonneg 📖	mathematical	Real instLE instZero	Real instMul iSup instSupSet	—	mul_comm mul_iSup_of_nonneg
iSup_mul_of_nonpos 📖	mathematical	Real instLE instZero	Real instMul iSup instSupSet iInf instInfSet	—	mul_comm mul_iSup_of_nonpos
mul_iInf_of_nonneg 📖	mathematical	Real instLE instZero	Real instMul iInf instInfSet	—	smul_iInf_of_nonneg instIsStrictOrderedRing IsStrictOrderedModule.toIsOrderedModule IsStrictOrderedRing.toIsStrictOrderedModule
mul_iInf_of_nonpos 📖	mathematical	Real instLE instZero	Real instMul iInf instInfSet iSup instSupSet	—	smul_iInf_of_nonpos instIsStrictOrderedRing IsStrictOrderedModule.toIsOrderedModule IsStrictOrderedRing.toIsStrictOrderedModule
mul_iSup_of_nonneg 📖	mathematical	Real instLE instZero	Real instMul iSup instSupSet	—	smul_iSup_of_nonneg instIsStrictOrderedRing IsStrictOrderedModule.toIsOrderedModule IsStrictOrderedRing.toIsStrictOrderedModule
mul_iSup_of_nonpos 📖	mathematical	Real instLE instZero	Real instMul iSup instSupSet iInf instInfSet	—	smul_iSup_of_nonpos instIsStrictOrderedRing IsStrictOrderedModule.toIsOrderedModule IsStrictOrderedRing.toIsStrictOrderedModule
sInf_smul_of_nonneg 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing	InfSet.sInf Real instInfSet Set Set.smulSet SMulZeroClass.toSMul instZero SMulWithZero.toSMulZeroClass MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield MulActionWithZero.toSMulWithZero	—	Set.eq_empty_or_nonempty Set.smul_set_empty sInf_empty smul_zero LE.le.eq_or_lt Set.zero_smul_set zero_smul csInf_singleton IsOrderedModule.toPosSMulMono PosSMulMono.toPosSMulReflectLE OrderIso.map_csInf' sInf_of_not_bddBelow bddBelow_smul_iff_of_pos
sInf_smul_of_nonpos 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing	InfSet.sInf Real instInfSet Set Set.smulSet SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass instAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Module.toDistribMulAction instAddCommMonoid SupSet.sSup instSupSet	—	Set.eq_empty_or_nonempty Set.smul_set_empty sInf_empty sSup_empty smul_zero LE.le.eq_or_lt Set.zero_smul_set zero_smul csInf_singleton instIsOrderedAddMonoid IsOrderedModule.toPosSMulMono OrderIso.map_csSup' sInf_of_not_bddBelow bddBelow_smul_iff_of_neg sSup_of_not_bddAbove
sSup_smul_of_nonneg 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing	SupSet.sSup Real instSupSet Set Set.smulSet SMulZeroClass.toSMul instZero SMulWithZero.toSMulZeroClass MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield MulActionWithZero.toSMulWithZero	—	Set.eq_empty_or_nonempty Set.smul_set_empty sSup_empty smul_zero LE.le.eq_or_lt Set.zero_smul_set zero_smul csSup_singleton IsOrderedModule.toPosSMulMono PosSMulMono.toPosSMulReflectLE OrderIso.map_csSup' sSup_of_not_bddAbove bddAbove_smul_iff_of_pos
sSup_smul_of_nonpos 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing	SupSet.sSup Real instSupSet Set Set.smulSet SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass instAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Module.toDistribMulAction instAddCommMonoid InfSet.sInf instInfSet	—	Set.eq_empty_or_nonempty Set.smul_set_empty sSup_empty sInf_empty smul_zero LE.le.eq_or_lt Set.zero_smul_set zero_smul csSup_singleton instIsOrderedAddMonoid IsOrderedModule.toPosSMulMono OrderIso.map_csInf' sSup_of_not_bddAbove bddAbove_smul_iff_of_neg sInf_of_not_bddBelow
smul_iInf_of_nonneg 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing	Real SMulZeroClass.toSMul instZero SMulWithZero.toSMulZeroClass MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield MulActionWithZero.toSMulWithZero iInf instInfSet	—	sInf_smul_of_nonneg Set.range_comp
smul_iInf_of_nonpos 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing	Real SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass instAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Module.toDistribMulAction instAddCommMonoid iInf instInfSet iSup instSupSet	—	sSup_smul_of_nonpos Set.range_comp
smul_iSup_of_nonneg 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing	Real SMulZeroClass.toSMul instZero SMulWithZero.toSMulZeroClass MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield MulActionWithZero.toSMulWithZero iSup instSupSet	—	sSup_smul_of_nonneg Set.range_comp
smul_iSup_of_nonpos 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing	Real SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass instAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Module.toDistribMulAction instAddCommMonoid iSup instSupSet iInf instInfSet	—	sInf_smul_of_nonpos Set.range_comp

---

← Back to Index