Documentation Verification Report

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`	`instMul` `iInf` `instInfSet`	—	`mul_comm` `mul_iInf_of_nonneg`
`iInf_mul_of_nonpos` 📖	mathematical	`Real` `instLE` `instZero`	`instMul` `iInf` `instInfSet` `iSup` `instSupSet`	—	`mul_comm` `mul_iInf_of_nonpos`
`iSup_mul_of_nonneg` 📖	mathematical	`Real` `instLE` `instZero`	`instMul` `iSup` `instSupSet`	—	`mul_comm` `mul_iSup_of_nonneg`
`iSup_mul_of_nonpos` 📖	mathematical	`Real` `instLE` `instZero`	`instMul` `iSup` `instSupSet` `iInf` `instInfSet`	—	`mul_comm` `mul_iSup_of_nonpos`
`mul_iInf_of_nonneg` 📖	mathematical	`Real` `instLE` `instZero`	`instMul` `iInf` `instInfSet`	—	`smul_iInf_of_nonneg` `instIsStrictOrderedRing` `IsStrictOrderedModule.toIsOrderedModule` `IsStrictOrderedRing.toIsStrictOrderedModule`
`mul_iInf_of_nonpos` 📖	mathematical	`Real` `instLE` `instZero`	`instMul` `iInf` `instInfSet` `iSup` `instSupSet`	—	`smul_iInf_of_nonpos` `instIsStrictOrderedRing` `IsStrictOrderedModule.toIsOrderedModule` `IsStrictOrderedRing.toIsStrictOrderedModule`
`mul_iSup_of_nonneg` 📖	mathematical	`Real` `instLE` `instZero`	`instMul` `iSup` `instSupSet`	—	`smul_iSup_of_nonneg` `instIsStrictOrderedRing` `IsStrictOrderedModule.toIsOrderedModule` `IsStrictOrderedRing.toIsStrictOrderedModule`
`mul_iSup_of_nonpos` 📖	mathematical	`Real` `instLE` `instZero`	`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` `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` `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` `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` `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