Pointwise

📁 Source: Mathlib/Algebra/Order/Module/Pointwise.lean

Statistics

Metric	Count
Definitions	0
Theorems smul_of_nonneg, smul_of_nonpos, smul_of_nonneg, smul_of_nonpos, bddAbove_smul_iff_of_neg, bddAbove_smul_iff_of_pos, bddBelow_smul_iff_of_neg, bddBelow_smul_iff_of_pos, lowerBounds_smul_of_neg, lowerBounds_smul_of_pos, smul_lowerBounds_subset_lowerBounds_smul_of_nonneg, smul_lowerBounds_subset_upperBounds_smul, smul_upperBounds_subset_lowerBounds_smul, smul_upperBounds_subset_upperBounds_smul_of_nonneg, upperBounds_smul_of_neg, upperBounds_smul_of_pos	16
Total	16

BddAbove

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
smul_of_nonneg 📖	mathematical	BddAbove Preorder.toLE	Set Set.smulSet	—	Monotone.map_bddAbove monotone_smul_left_of_nonneg
smul_of_nonpos 📖	mathematical	Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing BddAbove	BddBelow Set Set.smulSet SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Module.toDistribMulAction AddCommGroup.toAddCommMonoid	—	Antitone.map_bddAbove antitone_smul_left

BddBelow

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
smul_of_nonneg 📖	mathematical	BddBelow Preorder.toLE	Set Set.smulSet	—	Monotone.map_bddBelow monotone_smul_left_of_nonneg
smul_of_nonpos 📖	mathematical	Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing BddBelow	BddAbove Set Set.smulSet SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Module.toDistribMulAction AddCommGroup.toAddCommMonoid	—	Antitone.map_bddBelow antitone_smul_left

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bddAbove_smul_iff_of_neg 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing	BddAbove Preorder.toLE Set Set.smulSet SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Module.toDistribMulAction AddCommGroup.toAddCommMonoid BddBelow	—	OrderIso.bddBelow_image
bddAbove_smul_iff_of_pos 📖	mathematical	Preorder.toLT MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero	BddAbove Preorder.toLE Set Set.smulSet SMulZeroClass.toSMul SMulWithZero.toSMulZeroClass MulActionWithZero.toSMulWithZero	—	OrderIso.bddAbove_image
bddBelow_smul_iff_of_neg 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing	BddBelow Preorder.toLE Set Set.smulSet SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Module.toDistribMulAction AddCommGroup.toAddCommMonoid BddAbove	—	OrderIso.bddAbove_image
bddBelow_smul_iff_of_pos 📖	mathematical	Preorder.toLT MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero	BddBelow Preorder.toLE Set Set.smulSet SMulZeroClass.toSMul SMulWithZero.toSMulZeroClass MulActionWithZero.toSMulWithZero	—	OrderIso.bddBelow_image
lowerBounds_smul_of_neg 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing	lowerBounds Preorder.toLE Set Set.smulSet SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Module.toDistribMulAction AddCommGroup.toAddCommMonoid upperBounds	—	OrderIso.upperBounds_image
lowerBounds_smul_of_pos 📖	mathematical	Preorder.toLT MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero	lowerBounds Preorder.toLE Set Set.smulSet SMulZeroClass.toSMul SMulWithZero.toSMulZeroClass MulActionWithZero.toSMulWithZero	—	OrderIso.lowerBounds_image
smul_lowerBounds_subset_lowerBounds_smul_of_nonneg 📖	mathematical	Preorder.toLE	Set Set.instHasSubset Set.smulSet lowerBounds	—	Monotone.image_lowerBounds_subset_lowerBounds_image monotone_smul_left_of_nonneg
smul_lowerBounds_subset_upperBounds_smul 📖	mathematical	Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	Set Set.instHasSubset Set.smulSet SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Module.toDistribMulAction AddCommGroup.toAddCommMonoid lowerBounds upperBounds	—	Antitone.image_lowerBounds_subset_upperBounds_image antitone_smul_left
smul_upperBounds_subset_lowerBounds_smul 📖	mathematical	Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	Set Set.instHasSubset Set.smulSet SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Module.toDistribMulAction AddCommGroup.toAddCommMonoid upperBounds lowerBounds	—	Antitone.image_upperBounds_subset_lowerBounds_image antitone_smul_left
smul_upperBounds_subset_upperBounds_smul_of_nonneg 📖	mathematical	Preorder.toLE	Set Set.instHasSubset Set.smulSet upperBounds	—	Monotone.image_upperBounds_subset_upperBounds_image monotone_smul_left_of_nonneg
upperBounds_smul_of_neg 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing	upperBounds Preorder.toLE Set Set.smulSet SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Module.toDistribMulAction AddCommGroup.toAddCommMonoid lowerBounds	—	OrderIso.lowerBounds_image
upperBounds_smul_of_pos 📖	mathematical	Preorder.toLT MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero	upperBounds Preorder.toLE Set Set.smulSet SMulZeroClass.toSMul SMulWithZero.toSMulZeroClass MulActionWithZero.toSMulWithZero	—	OrderIso.upperBounds_image

---

← Back to Index