convexHull_pi — Mathlib

English

For finite index sets, convex hull commutes with the pi-operation (coordinate-wise convex hull).

Русский

Для конечного множества индексов выпуклая оболочка коммутирует с операцией пи (координатная выпуклая оболочка).

LaTeX

$$$\operatorname{conv}(R, s.\,pi t) = s.\,pi (\lambda i. \operatorname{conv}(R, t_i))$$$

Lean4

@[simp]
theorem convexHull_pi (s : Set ι) (t : Π i, Set (E i)) : convexHull 𝕜 (s.pi t) = s.pi (fun i ↦ convexHull 𝕜 (t i)) :=
  Set.Subset.antisymm
    (convexHull_min (Set.pi_mono fun _ _ ↦ subset_convexHull _ _) <| convex_pi <| fun _ _ ↦ convex_convexHull _ _)
    fun _ ↦ mem_convexHull_pi

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