Star

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

Statistics

Metric	Count
Definitions `StarConvex`	1
Theorems `starConvex`, `add`, `add_left`, `add_right`, `add_smul_mem`, `add_smul_sub_mem`, `affine_image`, `affine_preimage`, `affinity`, `inter`, `is_linear_image`, `is_linear_preimage`, `linear_image`, `linear_preimage`, `mem`, `mem_smul`, `neg`, `openSegment_subset`, `ordConnected`, `preimage_add_left`, `preimage_add_right`, `preimage_smul`, `prod`, `segment_subset`, `smul`, `smul_mem`, `sub`, `sub'`, `union`, `zero_smul`, `starConvex_compl_Ici`, `starConvex_compl_Iic`, `starConvex_empty`, `starConvex_iInter`, `starConvex_iInter₂`, `starConvex_iUnion`, `starConvex_iUnion₂`, `starConvex_iff_div`, `starConvex_iff_forall_ne_pos`, `starConvex_iff_forall_pos`, `starConvex_iff_openSegment_subset`, `starConvex_iff_ordConnected`, `starConvex_iff_pointwise_add_subset`, `starConvex_iff_segment_subset`, `starConvex_pi`, `starConvex_sInter`, `starConvex_sUnion`, `starConvex_singleton`, `starConvex_univ`, `starConvex_zero_iff`	50
Total	51

Set.OrdConnected

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`starConvex` 📖	mathematical	`Set` `Set.instMembership` `Preorder.toLE` `PartialOrder.toPreorder`	`StarConvex` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	—	`out` `Set.mem_Icc` `Convex.combo_self` `add_le_add_right` `IsOrderedAddMonoid.toAddLeftMono` `smul_le_smul_of_nonneg_left` `add_le_add_left` `covariant_swap_add_of_covariant_add`

StarConvex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add` 📖	mathematical	`StarConvex` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `Set` `Set.add`	—	`Set.add_image_prod` `is_linear_image` `prod` `IsLinearMap.isLinearMap_add`
`add_left` 📖	mathematical	`StarConvex` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `Set.image`	—	`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`
`add_right` 📖	mathematical	`StarConvex` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `Set.image`	—	`Mathlib.Tactic.Module.NF.eq_of_eval_eq_eval` `Mathlib.Tactic.Module.NF.add_eq_eval` `Mathlib.Tactic.Module.NF.smul_eq_eval` `Mathlib.Tactic.Module.NF.atom_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.add_eq_eval₂` `Mathlib.Tactic.Module.NF.eq_cons_cons` `eq_natCast` `RingHom.instRingHomClass` `Nat.cast_one` `mul_one`
`add_smul_mem` 📖	—	`StarConvex` `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.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	—	—	`smul_add` `add_assoc` `add_smul` `sub_add_cancel` `one_smul` `sub_nonneg_of_le`
`add_smul_sub_mem` 📖	mathematical	`StarConvex` `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.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `SubNegMonoid.toSub`	—	`segment_subset` `segment_eq_image'` `Set.mem_image_of_mem`
`affine_image` 📖	mathematical	`StarConvex` `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`	`DFunLike.coe` `AffineMap` `addGroupIsAddTorsor` `AffineMap.instFunLike` `Set.image`	—	`Convex.combo_affine_apply`
`affine_preimage` 📖	mathematical	`StarConvex` `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` `DFunLike.coe` `AffineMap` `addGroupIsAddTorsor` `AffineMap.instFunLike`	`Set.preimage`	—	`Set.mem_preimage` `Convex.combo_affine_apply`
`affinity` 📖	mathematical	`StarConvex` `CommSemiring.toSemiring` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `Set.image`	—	`add_left` `smul` `Set.image_image` `Set.image_smul`
`inter` 📖	mathematical	`StarConvex`	`Set` `Set.instInter`	—	—
`is_linear_image` 📖	mathematical	`StarConvex` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `IsLinearMap`	`Set.image`	—	`linear_image`
`is_linear_preimage` 📖	mathematical	`StarConvex` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `IsLinearMap`	`Set.preimage`	—	`linear_preimage`
`linear_image` 📖	mathematical	`StarConvex` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike` `Set.image`	—	`LinearMap.map_add` `LinearMap.map_smul`
`linear_preimage` 📖	mathematical	`StarConvex` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike`	`Set.preimage`	—	`Set.mem_preimage` `LinearMap.map_add` `LinearMap.map_smul`
`mem` 📖	mathematical	`StarConvex` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Set.Nonempty`	`Set` `Set.instMembership`	—	`one_smul` `zero_smul` `add_zero` `zero_le_one` `le_rfl`
`mem_smul` 📖	mathematical	`StarConvex` `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` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Set` `Set.instMembership` `Preorder.toLE` `PartialOrder.toPreorder` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing`	`Set.smulSet`	—	`Set.mem_smul_set_iff_inv_smul_mem₀` `LT.lt.ne'` `LT.lt.trans_le` `zero_lt_one` `IsStrictOrderedRing.toZeroLEOneClass` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `smul_mem` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `le_of_lt` `inv_pos_of_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `lt_of_lt_of_le` `Mathlib.Meta.Positivity.pos_of_isNat` `instNontrivialOfCharZero` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `inv_le_one_of_one_le₀`
`neg` 📖	mathematical	`StarConvex` `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`	`NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Set` `Set.neg`	—	`Set.image_neg_eq_neg` `is_linear_image` `IsLinearMap.isLinearMap_neg`
`openSegment_subset` 📖	mathematical	`StarConvex` `Set` `Set.instMembership`	`Set.instHasSubset` `openSegment`	—	`HasSubset.Subset.trans` `Set.instIsTransSubset` `openSegment_subset_segment` `segment_subset`
`ordConnected` 📖	mathematical	`Set` `Set.instMembership` `StarConvex` `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`	—	`starConvex_iff_ordConnected`
`preimage_add_left` 📖	mathematical	`StarConvex` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	`Set.preimage`	—	`add_comm` `preimage_add_right`
`preimage_add_right` 📖	mathematical	`StarConvex` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	`Set.preimage`	—	`one_smul` `add_smul` `add_add_add_comm` `smul_add`
`preimage_smul` 📖	mathematical	`StarConvex` `CommSemiring.toSemiring` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	`Set.preimage`	—	`linear_preimage` `smulCommClass_self`
`prod` 📖	mathematical	`StarConvex`	`Prod.instAddCommMonoid` `Prod.instSMul` `SProd.sprod` `Set` `Set.instSProd`	—	—
`segment_subset` 📖	mathematical	`StarConvex` `Set` `Set.instMembership`	`Set.instHasSubset` `segment`	—	`starConvex_iff_segment_subset`
`smul` 📖	mathematical	`StarConvex` `CommSemiring.toSemiring` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	`Set` `Set.smulSet`	—	`linear_image` `smulCommClass_self`
`smul_mem` 📖	—	`StarConvex` `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` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Set` `Set.instMembership` `Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	—	—	`zero_add` `add_smul_mem`
`sub` 📖	mathematical	`StarConvex` `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`	`SubNegMonoid.toSub` `Set` `Set.sub`	—	`sub_eq_add_neg` `add` `neg`
`sub'` 📖	mathematical	`StarConvex` `Prod.instAddCommMonoid` `AddCommGroup.toAddCommMonoid` `Prod.instSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	`SubNegMonoid.toSub` `Set.image`	—	`is_linear_image` `IsLinearMap.isLinearMap_sub`
`union` 📖	mathematical	`StarConvex`	`Set` `Set.instUnion`	—	—
`zero_smul` 📖	mathematical	`StarConvex` `CommSemiring.toSemiring` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	`Set` `Set.smulSet`	—	`smul_zero` `smul`

(root)

Definitions

Name	Category	Theorems
`StarConvex` 📖	MathDef	21 math math: `starConvex_iff_ordConnected`, `Complex.starConvex_ofReal_slitPlane`, `Complex.starConvex_one_slitPlane`, `starConvex_compl_Ici`, `starConvex_iff_pointwise_add_subset`, `starConvex_iff_forall_ne_pos`, `starConvex_iff_segment_subset`, `starConvex_iff_openSegment_subset`, `starConvex_zero_iff`, `Submodule.starConvex`, `starConvex_singleton`, `Balanced.starConvex`, `starConvex_iff_forall_pos`, `Complex.starConvex_slitPlane`, `Convex.starConvex_iff`, `Convex.starConvex`, `Set.OrdConnected.starConvex`, `starConvex_compl_Iic`, `starConvex_univ`, `starConvex_empty`, `starConvex_iff_div`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`starConvex_compl_Ici` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder`	`StarConvex` `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` `Compl.compl` `Set` `Set.instCompl` `Set.Ici`	—	`starConvex_compl_Iic` `OrderDual.isOrderedAddMonoid` `AddCommGroup.add_comm` `OrderDual.instIsStrictOrderedModule` `OrderDual.instPosSMulReflectLT`
`starConvex_compl_Iic` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder`	`StarConvex` `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` `Compl.compl` `Set` `Set.instCompl` `Set.Iic`	—	`starConvex_iff_forall_pos` `LT.lt.not_ge` `Set.mem_compl_iff` `Set.mem_Iic` `Mathlib.Tactic.Contrapose.contrapose₄` `LT.lt.le` `lt_of_smul_lt_smul_of_nonneg_left` `le_sub_iff_add_le'` `IsOrderedAddMonoid.toAddLeftMono` `one_smul` `add_smul` `sub_lt_iff_lt_add'` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `add_lt_add_left` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `smul_lt_smul_of_pos_left` `IsStrictOrderedModule.toPosSMulStrictMono`
`starConvex_empty` 📖	mathematical	—	`StarConvex` `Set` `Set.instEmptyCollection`	—	—
`starConvex_iInter` 📖	mathematical	`StarConvex`	`Set.iInter`	—	`starConvex_sInter` `Set.sInter_range` `Set.forall_mem_range`
`starConvex_iInter₂` 📖	mathematical	`StarConvex`	`Set.iInter`	—	`starConvex_iInter`
`starConvex_iUnion` 📖	mathematical	`StarConvex`	`Set.iUnion`	—	`Set.mem_iUnion`
`starConvex_iUnion₂` 📖	mathematical	`StarConvex`	`Set.iUnion`	—	`starConvex_iUnion`
`starConvex_iff_div` 📖	mathematical	—	`StarConvex` `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` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `Field.toDivisionRing` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing`	—	`Mathlib.Meta.Positivity.div_nonneg_of_nonneg_of_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `add_div` `div_self` `LT.lt.ne'` `div_one` `zero_lt_one` `IsStrictOrderedRing.toZeroLEOneClass` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero`
`starConvex_iff_forall_ne_pos` 📖	mathematical	`Set` `Set.instMembership`	`StarConvex` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	`LT.lt.le` `LE.le.eq_or_lt` `zero_add` `zero_smul` `one_smul` `add_zero` `eq_or_ne` `Convex.combo_self`
`starConvex_iff_forall_pos` 📖	mathematical	`Set` `Set.instMembership`	`StarConvex` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	`LT.lt.le` `LE.le.eq_or_lt` `zero_add` `one_smul` `zero_smul` `add_zero`
`starConvex_iff_openSegment_subset` 📖	mathematical	`Set` `Set.instMembership`	`StarConvex` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Set.instHasSubset` `openSegment`	—	`starConvex_iff_segment_subset` `openSegment_subset_iff_segment_subset`
`starConvex_iff_ordConnected` 📖	mathematical	`Set` `Set.instMembership`	`StarConvex` `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`	—	`Set.ordConnected_iff_uIcc_subset_left` `segment_eq_uIcc`
`starConvex_iff_pointwise_add_subset` 📖	mathematical	—	`StarConvex` `Set` `Set.instHasSubset` `Set.add` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `Set.smulSet` `Set.instSingletonSet`	—	`Set.add_mem_add` `Set.smul_mem_smul_set` `Set.mem_singleton`
`starConvex_iff_segment_subset` 📖	mathematical	—	`StarConvex` `Set` `Set.instHasSubset` `segment`	—	—
`starConvex_pi` 📖	mathematical	`StarConvex`	`Pi.addCommMonoid` `Pi.instSMul` `Set.pi`	—	—
`starConvex_sInter` 📖	mathematical	`StarConvex`	`Set.sInter`	—	—
`starConvex_sUnion` 📖	mathematical	`StarConvex`	`Set.sUnion`	—	`Set.sUnion_eq_iUnion` `starConvex_iUnion`
`starConvex_singleton` 📖	mathematical	—	`StarConvex` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Set` `Set.instSingletonSet`	—	`Convex.combo_self`
`starConvex_univ` 📖	mathematical	—	`StarConvex` `Set.univ`	—	—
`starConvex_zero_iff` 📖	mathematical	—	`StarConvex` `Ring.toSemiring` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `SMulWithZero.toSMulZeroClass` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Set` `Set.instMembership`	—	`sub_add_cancel` `smul_zero` `zero_add` `sub_nonneg_of_le` `le_add_of_nonneg_left`

---

← Back to Index