Mathlib Map

Theorems · Theorem · convex and discrete geometry

Convex.starConvex

∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : SMul 𝕜 E] {s : Set E} {x : E}, Convex 𝕜 s → x ∈ s → StarConvex 𝕜 x s
Defined in
Mathlib.Analysis.Convex.Basic
Cited by
4 results in Mathlib
Foundations
Depth 14 from the axioms · uses no axioms
Assumes
SemiringPartialOrderAddCommMonoidSMul
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Convex.contractibleSpace · cited by 3Convex.contractibleSpaceseparate_convex_open_set · cited by 2separate_convex_open_setconvexHull_sphere_eq_closedBall · cited by 1convexHull_sphere_eq_clos…Convex.starConvex_iff · cited by 0Convex.starConvex_iffSet · cited by 53352SetSemiring · cited by 13802SemiringAddCommMonoid · cited by 12281AddCommMonoidPartialOrder · cited by 6410PartialOrderConvex · cited by 551ConvexStarConvex · cited by 62StarConvexConvex.starConvexCITED BYCITES

Cites6

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • Setstatement and proof · cited by 53,352
  • Semiringstatement and proof · cited by 13,802
  • AddCommMonoidstatement and proof · cited by 12,281
  • PartialOrderstatement and proof · cited by 6,410
  • Convexstatement and proof · cited by 551
  • StarConvexstatement · cited by 62

Cited by4

Results whose statement or proof uses this declaration.