Strict

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

Statistics

Metric	Count
Definitions StrictConvex	1
Theorems strictConvex_of_isOpen, strictConvex_iUnion, strictConvex_sUnion, strictConvex_iff, strictConvex, strictConvex, add, add_left, add_right, add_smul_mem, add_smul_sub_mem, affine_image, affine_preimage, affinity, convex, eq, eq_of_openSegment_subset_frontier, inter, is_linear_image, is_linear_preimage, linear_image, linear_preimage, mem_smul_of_zero_mem, neg, openSegment_subset, ordConnected, preimage_add_left, preimage_add_right, preimage_smul, smul, smul_mem_of_zero_mem, sub, vadd, strictConvex_Icc, strictConvex_Ici, strictConvex_Ico, strictConvex_Iic, strictConvex_Iio, strictConvex_Ioc, strictConvex_Ioi, strictConvex_Ioo, strictConvex_empty, strictConvex_iff_convex, strictConvex_iff_div, strictConvex_iff_openSegment_subset, strictConvex_iff_ordConnected, strictConvex_singleton, strictConvex_uIcc, strictConvex_uIoc, strictConvex_univ	50
Total	51

Convex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
strictConvex_of_isOpen 📖	mathematical	IsOpen Convex SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	StrictConvex	—	LT.lt.le IsOpen.interior_eq

Directed

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
strictConvex_iUnion 📖	mathematical	Directed Set Set.instHasSubset StrictConvex	Set.iUnion	—	Set.mem_iUnion interior_mono Set.subset_iUnion

DirectedOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
strictConvex_sUnion 📖	mathematical	DirectedOn Set Set.instHasSubset StrictConvex	Set.sUnion	—	Set.sUnion_eq_iUnion Directed.strictConvex_iUnion directedOn_iff_directed

IsOpen

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
strictConvex_iff 📖	mathematical	IsOpen	StrictConvex SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Convex	—	StrictConvex.convex Convex.strictConvex_of_isOpen

Set.OrdConnected

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
strictConvex 📖	mathematical	—	StrictConvex SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	strictConvex_iff_openSegment_subset Ne.lt_or_gt HasSubset.Subset.trans Set.instIsTransSubset openSegment_subset_Ioo IsOpen.subset_interior_iff isOpen_Ioo OrderTopology.to_orderClosedTopology Set.Ioo_subset_Icc_self out openSegment_symm

Set.Subsingleton

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
strictConvex 📖	mathematical	Set.Subsingleton	StrictConvex SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	pairwise

StrictConvex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add 📖	mathematical	StrictConvex AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	Set Set.add AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	smul_add add_add_add_comm eq_or_ne interior_mono Set.add_subset_add Set.singleton_subset_iff Set.Subset.rfl Convex.combo_self Set.singleton_add IsOpenMap.image_interior_subset isOpenMap_add_left Set.mem_image_of_mem subset_interior_add_left ContinuousConstVAdd.op VAddCommClass.continuousConstVAdd vaddCommClass_self AddCommSemigroup.isCentralVAdd Set.add_mem_add convex LT.lt.le
add_left 📖	mathematical	StrictConvex AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	Set.image AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	Set.singleton_add add strictConvex_singleton
add_right 📖	mathematical	StrictConvex AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	Set.image AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	Set.image_congr add_comm add_left
add_smul_mem 📖	mathematical	StrictConvex Ring.toSemiring AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Set Set.instMembership AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup Preorder.toLT PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	interior	—	Mathlib.Tactic.Module.NF.eq_of_eval_eq_eval Mathlib.Tactic.Module.NF.add_eq_eval Mathlib.Tactic.Module.NF.atom_eq_eval Mathlib.Tactic.Module.NF.smul_eq_eval Mathlib.Tactic.Module.NF.eval_algebraMap AddCommMonoid.nat_isScalarTower Mathlib.Tactic.Module.NF.add_eq_eval₁ zero_add Mathlib.Tactic.Module.NF.add_eq_eval₂ Mathlib.Tactic.Module.NF.eq_cons_cons eq_natCast RingHom.instRingHomClass Nat.cast_one mul_one sub_add_cancel add_left_cancel AddLeftCancelSemigroup.toIsLeftCancelAdd add_zero sub_pos_of_lt
add_smul_sub_mem 📖	mathematical	StrictConvex Ring.toSemiring AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Set Set.instMembership Preorder.toLT PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	interior AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup SubNegMonoid.toSub	—	openSegment_subset openSegment_eq_image' Set.mem_image_of_mem
affine_image 📖	mathematical	StrictConvex Ring.toSemiring AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction IsOpenMap DFunLike.coe AffineMap addGroupIsAddTorsor AffineMap.instFunLike	Set.image	—	IsOpenMap.image_interior_subset Convex.combo_affine_apply
affine_preimage 📖	mathematical	StrictConvex Ring.toSemiring AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Continuous DFunLike.coe AffineMap addGroupIsAddTorsor AffineMap.instFunLike	Set.preimage	—	preimage_interior_subset_interior_preimage Set.mem_preimage Convex.combo_affine_apply
affinity 📖	mathematical	StrictConvex AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	HVAdd.hVAdd Set instHVAdd Set.vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup AddAction.toAddSemigroupAction AddTorsor.toAddAction addGroupIsAddTorsor Set.smulSet DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield	—	vadd smul
convex 📖	mathematical	StrictConvex SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	Convex	—	convex_iff_pairwise_pos interior_subset
eq 📖	—	StrictConvex Set Set.instMembership Preorder.toLT PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne interior AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	—	Set.Pairwise.eq
eq_of_openSegment_subset_frontier 📖	—	StrictConvex Ring.toSemiring AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Set Set.instMembership Set.instHasSubset openSegment frontier	—	—	DenselyOrdered.dense zero_lt_one IsOrderedRing.toZeroLEOneClass NeZero.one sub_pos_of_lt IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid add_sub_cancel
inter 📖	mathematical	StrictConvex	Set Set.instInter	—	interior_inter
is_linear_image 📖	mathematical	StrictConvex SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction IsLinearMap IsOpenMap	Set.image	—	linear_image LinearMap.IsScalarTower.compatibleSMul IsScalarTower.left
is_linear_preimage 📖	mathematical	StrictConvex SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction IsLinearMap Continuous	Set.preimage	—	linear_preimage
linear_image 📖	mathematical	StrictConvex SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction IsOpenMap DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike	Set.image	—	IsOpenMap.image_interior_subset map_add SemilinearMapClass.toAddHomClass LinearMap.semilinearMapClass LinearMap.map_smul_of_tower
linear_preimage 📖	mathematical	StrictConvex SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Continuous DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike	Set.preimage	—	preimage_interior_subset_interior_preimage Set.mem_preimage LinearMap.map_add LinearMap.map_smul
mem_smul_of_zero_mem 📖	mathematical	StrictConvex DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Set Set.instMembership NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Preorder.toLT PartialOrder.toPreorder AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing	Set.smulSet interior	—	Set.mem_smul_set_iff_inv_smul_mem₀ ne_of_gt lt_trans Mathlib.Meta.Positivity.pos_of_isNat IsStrictOrderedRing.toIsOrderedRing instNontrivialOfCharZero IsStrictOrderedRing.toCharZero Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one smul_mem_of_zero_mem IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid inv_pos_of_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono inv_lt_one_of_one_lt₀ IsStrictOrderedRing.toZeroLEOneClass
neg 📖	mathematical	StrictConvex Ring.toSemiring AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	Set Set.neg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	is_linear_preimage IsLinearMap.isLinearMap_neg Continuous.neg IsTopologicalAddGroup.toContinuousNeg continuous_id neg_injective
openSegment_subset 📖	mathematical	StrictConvex Set Set.instMembership	Set.instHasSubset openSegment interior	—	strictConvex_iff_openSegment_subset
ordConnected 📖	mathematical	StrictConvex DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Algebra.toSMul Semifield.toCommSemiring CommSemiring.toSemiring Algebra.id	Set.OrdConnected PartialOrder.toPreorder	—	strictConvex_iff_ordConnected
preimage_add_left 📖	mathematical	StrictConvex AddCancelCommMonoid.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	Set.preimage AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	add_comm preimage_add_right
preimage_add_right 📖	mathematical	StrictConvex AddCancelCommMonoid.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	Set.preimage AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	preimage_interior_subset_interior_preimage continuous_add_left add_right_injective AddLeftCancelSemigroup.toIsLeftCancelAdd one_smul add_smul add_add_add_comm smul_add
preimage_smul 📖	mathematical	StrictConvex CommSemiring.toSemiring AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	Set.preimage	—	eq_or_ne zero_smul Set.preimage_const strictConvex_univ strictConvex_empty linear_preimage smulCommClass_self ContinuousConstSMul.continuous_const_smul smul_right_injective IsDomain.toIsCancelMulZero
smul 📖	mathematical	StrictConvex AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	Set Set.smulSet DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield	—	eq_or_ne Set.Subsingleton.strictConvex Set.subsingleton_zero_smul_set linear_image smulCommClass_self isOpenMap_smul₀
smul_mem_of_zero_mem 📖	mathematical	StrictConvex Ring.toSemiring AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Set Set.instMembership NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Preorder.toLT PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	interior	—	zero_add add_smul_mem
sub 📖	mathematical	StrictConvex Ring.toSemiring AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	Set Set.sub SubNegMonoid.toSub	—	add IsTopologicalAddGroup.toContinuousAdd neg sub_eq_add_neg
vadd 📖	mathematical	StrictConvex AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	HVAdd.hVAdd Set instHVAdd Set.vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup AddAction.toAddSemigroupAction AddTorsor.toAddAction addGroupIsAddTorsor	—	add_left

(root)

Definitions

Name	Category	Theorems
StrictConvex 📖	MathDef	30 math math: LinearIsometryEquiv.strictConvex_preimage, strictConvex_Iic, strictConvex_Icc, strictConvex_uIcc, strictConvex_closedBall, Convex.strictConvex, strictConvex_Ioo, strictConvex_iff_openSegment_subset, strictConvexSpace_iff, strictConvex_Iio, strictConvex_empty, strictConvex_iff_convex, Set.Subsingleton.strictConvex, strictConvex_Ici, StrictConvexSpace.strictConvex_closedBall, ContinuousLinearEquiv.strictConvex_image, LinearIsometryEquiv.strictConvex_image, Convex.strictConvex', strictConvex_Ioc, strictConvex_Ico, IsOpen.strictConvex_iff, strictConvex_iff_ordConnected, strictConvex_singleton, strictConvex_iff_div, Set.OrdConnected.strictConvex, Convex.strictConvex_of_isOpen, ContinuousLinearEquiv.strictConvex_preimage, strictConvex_uIoc, strictConvex_Ioi, strictConvex_univ

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
strictConvex_Icc 📖	mathematical	—	StrictConvex SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Set.Icc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	Set.OrdConnected.strictConvex Set.ordConnected_Icc
strictConvex_Ici 📖	mathematical	—	StrictConvex SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Set.Ici PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	Set.OrdConnected.strictConvex Set.ordConnected_Ici
strictConvex_Ico 📖	mathematical	—	StrictConvex SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Set.Ico PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	Set.OrdConnected.strictConvex Set.ordConnected_Ico
strictConvex_Iic 📖	mathematical	—	StrictConvex SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Set.Iic PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	Set.OrdConnected.strictConvex Set.ordConnected_Iic
strictConvex_Iio 📖	mathematical	—	StrictConvex SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Set.Iio PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	Set.OrdConnected.strictConvex Set.ordConnected_Iio
strictConvex_Ioc 📖	mathematical	—	StrictConvex SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Set.Ioc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	Set.OrdConnected.strictConvex Set.ordConnected_Ioc
strictConvex_Ioi 📖	mathematical	—	StrictConvex SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Set.Ioi PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	Set.OrdConnected.strictConvex Set.ordConnected_Ioi
strictConvex_Ioo 📖	mathematical	—	StrictConvex SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Set.Ioo PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	Set.OrdConnected.strictConvex Set.ordConnected_Ioo
strictConvex_empty 📖	mathematical	—	StrictConvex Set Set.instEmptyCollection	—	Set.pairwise_empty
strictConvex_iff_convex 📖	mathematical	—	StrictConvex DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Algebra.toSMul Semifield.toCommSemiring CommSemiring.toSemiring Algebra.id Convex	—	StrictConvex.convex Set.OrdConnected.strictConvex IsStrictOrderedRing.toIsOrderedCancelAddMonoid IsStrictOrderedModule.toPosSMulStrictMono IsStrictOrderedRing.toIsStrictOrderedModule Convex.ordConnected
strictConvex_iff_div 📖	mathematical	—	StrictConvex DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Set.Pairwise	—	div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono add_pos' IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.subst_add Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons one_mul Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div div_one Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂ Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero ne_of_gt Mathlib.Tactic.FieldSimp.NF.one_eq_eval one_ne_zero NeZero.one GroupWithZero.toNontrivial Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one
strictConvex_iff_openSegment_subset 📖	mathematical	—	StrictConvex Set.Pairwise Set Set.instHasSubset openSegment interior	—	openSegment_subset_iff
strictConvex_iff_ordConnected 📖	mathematical	—	StrictConvex DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Algebra.toSMul Semifield.toCommSemiring CommSemiring.toSemiring Algebra.id Set.OrdConnected PartialOrder.toPreorder	—	strictConvex_iff_convex convex_iff_ordConnected
strictConvex_singleton 📖	mathematical	—	StrictConvex SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Set Set.instSingletonSet	—	Set.pairwise_singleton
strictConvex_uIcc 📖	mathematical	—	StrictConvex SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Set.uIcc DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	strictConvex_Icc
strictConvex_uIoc 📖	mathematical	—	StrictConvex SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Set.uIoc	—	strictConvex_Ioc
strictConvex_univ 📖	mathematical	—	StrictConvex Set.univ	—	interior_univ Set.mem_univ

---

← Back to Index