Body

📁 Source: Mathlib/Analysis/Convex/Body.lean

Statistics

Metric	Count
Definitions carrier, instAdd, instAddCommMonoid, instAddMonoid, instDistribMulActionReal, instInhabited, instMetricSpace, instModuleNNReal, instPartialOrder, instPseudoMetricSpace, instSMulNat, instSMulReal, instSetLike, instZero	14
Theorems coe_add, coe_mk, coe_nsmul, coe_smul, coe_smul', coe_zero, convex, convex', ext, ext_iff, hausdorffDist_coe, hausdorffEDist_coe, hausdorffEDist_ne_top, hausdorffEdist_coe, hausdorffEdist_ne_top, iInter_smul_eq_self, isBounded, isClosed, isCompact, isCompact', nonempty, nonempty', smul_le_of_le, zero_mem_of_symmetric	24
Total	38

ConvexBody

Definitions

Name	Category	Theorems
carrier 📖	CompOp	3 math math: isCompact', convex', nonempty'
instAdd 📖	CompOp	1 math math: coe_add
instAddCommMonoid 📖	CompOp	—
instAddMonoid 📖	CompOp	2 math math: smul_le_of_le, coe_smul'
instDistribMulActionReal 📖	CompOp	2 math math: smul_le_of_le, coe_smul'
instInhabited 📖	CompOp	—
instMetricSpace 📖	CompOp	—
instModuleNNReal 📖	CompOp	—
instPartialOrder 📖	CompOp	1 math math: smul_le_of_le
instPseudoMetricSpace 📖	CompOp	3 math math: hausdorffDist_coe, hausdorffEDist_coe, hausdorffEdist_coe
instSMulNat 📖	CompOp	1 math math: coe_nsmul
instSMulReal 📖	CompOp	1 math math: coe_smul
instSetLike 📖	CompOp	15 math math: coe_smul, coe_mk, convex, ext_iff, isBounded, nonempty, isClosed, isCompact, hausdorffDist_coe, hausdorffEDist_coe, hausdorffEdist_coe, coe_add, coe_nsmul, coe_smul', coe_zero
instZero 📖	CompOp	1 math math: coe_zero

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_add 📖	mathematical	—	SetLike.coe ConvexBody AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul Real AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring instSetLike instAdd Set Set.add AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	—
coe_mk 📖	mathematical	Convex Real Real.semiring Real.partialOrder AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction IsCompact Set.Nonempty	SetLike.coe ConvexBody instSetLike	—	—
coe_nsmul 📖	mathematical	—	SetLike.coe ConvexBody AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul Real AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring instSetLike instSMulNat Set Set.NSMul NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	—
coe_smul 📖	mathematical	—	SetLike.coe ConvexBody AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul Real AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring instSetLike instSMulReal Set Set.smulSet	—	—
coe_smul' 📖	mathematical	—	SetLike.coe ConvexBody AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul Real AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring instSetLike NNReal instAddMonoid MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSemiringNNReal NNReal.instDistribMulActionOfReal instDistribMulActionReal Set Set.smulSet	—	—
coe_zero 📖	mathematical	—	SetLike.coe ConvexBody AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul Real AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring instSetLike instZero Set Set.zero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	—
convex 📖	mathematical	—	Convex Real Real.semiring Real.partialOrder AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction SetLike.coe ConvexBody instSetLike	—	convex'
convex' 📖	mathematical	—	Convex Real Real.semiring Real.partialOrder carrier	—	—
ext 📖	—	SetLike.coe ConvexBody AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul Real AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring instSetLike	—	—	SetLike.ext'
ext_iff 📖	mathematical	—	SetLike.coe ConvexBody AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul Real AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring instSetLike	—	ext
hausdorffDist_coe 📖	mathematical	—	Metric.hausdorffDist SeminormedAddCommGroup.toPseudoMetricSpace SetLike.coe ConvexBody UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup SMulZeroClass.toSMul Real AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring NormedSpace.toModule Real.normedField instSetLike Dist.dist PseudoMetricSpace.toDist instPseudoMetricSpace	—	—
hausdorffEDist_coe 📖	mathematical	—	Metric.hausdorffEDist PseudoMetricSpace.toPseudoEMetricSpace SeminormedAddCommGroup.toPseudoMetricSpace SetLike.coe ConvexBody UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup SMulZeroClass.toSMul Real AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring NormedSpace.toModule Real.normedField instSetLike EDist.edist PseudoEMetricSpace.toEDist instPseudoMetricSpace	—	edist_dist ENNReal.ofReal_toReal hausdorffEDist_ne_top
hausdorffEDist_ne_top 📖	—	—	—	—	Metric.hausdorffEDist_ne_top_of_nonempty_of_bounded nonempty isBounded
hausdorffEdist_coe 📖	mathematical	—	Metric.hausdorffEDist PseudoMetricSpace.toPseudoEMetricSpace SeminormedAddCommGroup.toPseudoMetricSpace SetLike.coe ConvexBody UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup SMulZeroClass.toSMul Real AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring NormedSpace.toModule Real.normedField instSetLike EDist.edist PseudoEMetricSpace.toEDist instPseudoMetricSpace	—	hausdorffEDist_coe
hausdorffEdist_ne_top 📖	—	—	—	—	hausdorffEDist_ne_top
iInter_smul_eq_self 📖	mathematical	ConvexBody UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup SMulZeroClass.toSMul Real AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring NormedSpace.toModule Real.normedField SetLike.instMembership instSetLike NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Filter.Tendsto NNReal Filter.atTop Nat.instPreorder nhds NNReal.instTopologicalSpace instZeroNNReal	Set.iInter Set Set.smulSet Real.instAdd Real.instOne NNReal.toReal SetLike.coe	—	Set.ext Bornology.IsBounded.exists_pos_norm_le isBounded IsClosed.closure_eq isClosed SeminormedAddCommGroup.mem_closure_iff NormedAddCommGroup.tendsto_atTop instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat NNReal.tendsto_coe div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Set.mem_smul_set Set.mem_iInter add_smul one_smul add_sub_cancel_left norm_smul NormedSpace.toNormSMulClass Real.norm_eq_abs lt_of_le_of_lt mul_le_mul_of_nonneg_left IsOrderedRing.toPosMulMono Real.instIsOrderedRing abs_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add sub_zero NNReal.coe_zero mul_comm lt_div_iff₀' le_rfl Convex.mem_smul_of_zero_mem convex le_add_of_nonneg_right NNReal.coe_nonneg
isBounded 📖	mathematical	—	Bornology.IsBounded PseudoMetricSpace.toBornology SeminormedAddCommGroup.toPseudoMetricSpace SetLike.coe ConvexBody UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup SMulZeroClass.toSMul Real AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring NormedSpace.toModule Real.normedField instSetLike	—	IsCompact.isBounded isCompact
isClosed 📖	mathematical	—	IsClosed SetLike.coe ConvexBody AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul Real AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring instSetLike	—	IsCompact.isClosed isCompact
isCompact 📖	mathematical	—	IsCompact SetLike.coe ConvexBody AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul Real AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring instSetLike	—	isCompact'
isCompact' 📖	mathematical	—	IsCompact carrier	—	—
nonempty 📖	mathematical	—	Set.Nonempty SetLike.coe ConvexBody AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul Real AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring instSetLike	—	nonempty'
nonempty' 📖	mathematical	—	Set.Nonempty carrier	—	—
smul_le_of_le 📖	mathematical	ConvexBody AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul Real AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring SetLike.instMembership instSetLike NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal	instPartialOrder instAddMonoid MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSemiringNNReal NNReal.instDistribMulActionOfReal instDistribMulActionReal	—	SetLike.coe_subset_coe instIsConcreteLE coe_smul' eq_zero_or_pos NNReal.instCanonicallyOrderedAdd Set.zero_smul_set nonempty Set.zero_subset Set.mem_smul_set smul_zero Set.mem_inv_smul_set_iff₀ LT.lt.ne' smul_smul Convex.mem_smul_of_zero_mem Real.instIsStrictOrderedRing convex le_inv_mul_iff₀ PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE LinearOrderedCommMonoidWithZero.toPosMulStrictMono mul_one
zero_mem_of_symmetric 📖	mathematical	ConvexBody AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul Real AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring SetLike.instMembership instSetLike NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	NegZeroClass.toZero	—	nonempty Nat.instAtLeastTwoHAddOfNat one_div smul_neg add_neg_cancel convex_iff_forall_pos convex lt_of_not_ge Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Real.instIsStrictOrderedRing neg_neg_of_pos Real.instIsOrderedAddMonoid Mathlib.Tactic.Linarith.zero_lt_one Mathlib.Meta.NormNum.instAtLeastTwo CancelDenoms.derive_trans Mathlib.Meta.NormNum.IsNNRat.to_eq Mathlib.Meta.NormNum.IsRat.to_isNNRat Mathlib.Meta.NormNum.isRat_sub Mathlib.Meta.NormNum.IsNNRat.to_isRat Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNNRat_inv_pos IsStrictOrderedRing.toCharZero CancelDenoms.div_subst Mathlib.Meta.NormNum.isNat_eq_true Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNat_mul Mathlib.Tactic.Linarith.mul_nonpos Real.instIsOrderedRing Mathlib.Tactic.Linarith.sub_nonpos_of_le Mathlib.Meta.NormNum.isNat_lt_true Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt Mathlib.Tactic.Linarith.without_one_mul Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.isInt_sub Mathlib.Meta.NormNum.isNNRat_add Mathlib.Tactic.Linarith.sub_neg_of_lt

---

← Back to Index