Theorems · Theorem · convex and discrete geometry

Convex.helly_theorem_compact

∀ {ι : Type u_1} {𝕜 : Type u_2} {E : Type u_3} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] [FiniteDimensional 𝕜 E] [inst_6 : TopologicalSpace E] [T2Space E]
  {F : ι → Set E},
  ↑(Module.finrank 𝕜 E) + 1 ≤ ENat.card ι →
    (∀ (i : ι), Convex 𝕜 (F i)) →
      (∀ (i : ι), IsCompact (F i)) →
        (∀ (I : Finset ι), I.card = Module.finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty) → (⋂ i, F i).Nonempty

Helly's theorem for families of compact convex sets in its classical form. If F is a (possibly infinite) family of more than d + 1 compact convex sets in a vector space of finite dimension d, and any d + 1 sets of F intersect nontrivially, then all sets of F intersect nontrivially.

Defined in

Mathlib.Analysis.Convex.Radon

Cited by

0 results in Mathlib

Foundations

Depth 125 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldLinearOrderIsStrictOrderedRingAddCommGroupModuleFiniteDimensionalTopologicalSpaceT2Space