convex — Mathlib

English

If B is exposed in A and A is convex, then B is convex.

Русский

Если B экспонировано относительно A и A выпукло, то B выпукло.

LaTeX

$$$$ IsExposed\ 𝕜\ A\ B \wedge Convex\ 𝕜\ A \Rightarrow Convex\ 𝕜\ B. $$$$

Lean4

protected theorem convex (hAB : IsExposed 𝕜 A B) (hA : Convex 𝕜 A) : Convex 𝕜 B :=
  by
  obtain rfl | hB := B.eq_empty_or_nonempty
  · exact convex_empty
  obtain ⟨l, rfl⟩ := hAB hB
  exact fun x₁ hx₁ x₂ hx₂ a b ha hb hab =>
    ⟨hA hx₁.1 hx₂.1 ha hb hab, fun y hy =>
      ((l.toLinearMap.concaveOn convex_univ).convex_ge _ ⟨mem_univ _, hx₁.2 y hy⟩ ⟨mem_univ _, hx₂.2 y hy⟩ ha hb hab).2⟩

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