English
The image of a strictly convex set under an affine map is strictly convex.
Русский
Образ строго выпуклого множества под аффинным отображением сохраняет строгую выпуклость.
LaTeX
$$$\StrictConvex 𝕜 s \rightarrow \forall {f : AffineMap 𝕜 E F}, IsOpenMap (f) \rightarrow \StrictConvex 𝕜 (Set.image (f) s)$$$
Lean4
/-- Alternative definition of set strict convexity, using division. -/
theorem strictConvex_iff_div :
StrictConvex 𝕜 s ↔
s.Pairwise fun x y => ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → (a / (a + b)) • x + (b / (a + b)) • y ∈ interior s :=
⟨fun h x hx y hy hxy a b ha hb ↦ h hx hy hxy (by positivity) (by positivity) (by field_simp),
fun h x hx y hy hxy a b ha hb hab ↦ by convert h hx hy hxy ha hb <;> rw [hab, div_one]⟩
