convexBodyLT'_convex — Mathlib

English

If x belongs to convexBodyLT', then -x belongs to convexBodyLT'.

Русский

Если x ∈ convexBodyLT', то -x ∈ convexBodyLT'.

LaTeX

$$$$ x \in convexBodyLT'(K,f,w_0) \Rightarrow -x \in convexBodyLT'(K,f,w_0). $$$$

Lean4

theorem convexBodyLT'_convex : Convex ℝ (convexBodyLT' K f w₀) :=
  by
  refine Convex.prod (convex_pi (fun _ _ => convex_ball _ _)) (convex_pi (fun _ _ => ?_))
  split_ifs
  · simp_rw [abs_lt]
    refine
      Convex.inter ((convex_halfSpace_re_gt _).inter (convex_halfSpace_re_lt _))
        ((convex_halfSpace_im_gt _).inter (convex_halfSpace_im_lt _))
  · exact convex_ball _ _

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