prod — Mathlib

English

The product of two star-convex sets is star-convex in the product space.

Русский

Произведение двух звездообразных множеств звездообразно в произведённом пространстве.

LaTeX

$$$$StarConvex_{\mathbb{K}}(x,y)\ s \rightarrow\ StarConvex_{\mathbb{K}}( (x,y), s \times\text{ᵀ} t ).$$$$

Lean4

theorem prod {y : F} {s : Set E} {t : Set F} (hs : StarConvex 𝕜 x s) (ht : StarConvex 𝕜 y t) :
    StarConvex 𝕜 (x, y) (s ×ˢ t) := fun _ hy _ _ ha hb hab => ⟨hs hy.1 ha hb hab, ht hy.2 ha hb hab⟩

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