convex_pi — Mathlib

English

If each t(i) is convex for i in s, then the Cartesian product over i in s of t(i) is convex.

Русский

Если для каждого i из множества s множество t(i) выпукло, тогда их произведение по индексу i ∈ s выпукло.

LaTeX

$$$\left( \forall i \in s, \ Convex 𝕜 (t(i)) \right) \to \Convex 𝕜 (s \pi t)$$$

Lean4

theorem convex_pi {ι : Type*} {E : ι → Type*} [∀ i, AddCommMonoid (E i)] [∀ i, SMul 𝕜 (E i)] {s : Set ι}
    {t : ∀ i, Set (E i)} (ht : ∀ ⦃i⦄, i ∈ s → Convex 𝕜 (t i)) : Convex 𝕜 (s.pi t) := fun _ hx =>
  starConvex_pi fun _ hi => ht hi <| hx _ hi

Похожие утверждения