English
Star-convexity is preserved coordinatewise in product spaces: if each x_i is in an appropriate star-convex set t_i, then the function x = (x_i) is star-convex with respect to the product of the t_i.
Русский
Звездообразность сохраняется по координатам в произведении пространств: если для каждого i соответствующая пара звездообразна, то и вся комбинация координат звездообразна.
LaTeX
$$$$\forall i,\ StarConvex_{\mathbb{K}}(x_i, t_i) \Rightarrow StarConvex_{\mathbb{K}}( (x_i)_{i}, (\, t_i\,)_{i} ).$$$$
Lean4
theorem starConvex_pi {ι : Type*} {E : ι → Type*} [∀ i, AddCommMonoid (E i)] [∀ i, SMul 𝕜 (E i)] {x : ∀ i, E i}
{s : Set ι} {t : ∀ i, Set (E i)} (ht : ∀ ⦃i⦄, i ∈ s → StarConvex 𝕜 (x i) (t i)) : StarConvex 𝕜 x (s.pi t) :=
fun _ hy _ _ ha hb hab i hi => ht hi (hy i hi) ha hb hab
