Theorems · Theorem · convex and discrete geometry

Convexity.IsConvexSet.pi

∀ {ι : Type u_1} {R : Type u_3} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R]
  {X : ι → Type u_7} [inst_3 : (i : ι) → Convexity.ConvexSpace R (X i)] {s : Set ι} {t : (i : ι) → Set (X i)},
  (∀ i ∈ s, Convexity.IsConvexSet R (t i)) → Convexity.IsConvexSet R (s.pi t)

Defined in

Mathlib.Geometry.Convex.Set

Cited by

0 results in Mathlib

Foundations

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

Assumes

SemiringPartialOrderIsStrictOrderedRingConvexity.ConvexSpace