English
Images of ample sets under continuous affine equivalences are ample.
Русский
Образы ампельных множеств под непрерывными аффинными эквивалентами ампельны.
LaTeX
$$$\mathrm{AmpleSet}(s) \rightarrow \mathrm{AmpleSet}(L''s)$$$
Lean4
/-- Images of ample sets under continuous affine equivalences are ample. -/
theorem image {s : Set E} (h : AmpleSet s) (L : E ≃ᴬ[ℝ] F) : AmpleSet (L '' s) :=
forall_mem_image.mpr fun x hx ↦
calc
(convexHull ℝ) (connectedComponentIn (L '' s) (L x))
_ = (convexHull ℝ) (L '' (connectedComponentIn s x)) :=
(.symm <| congrArg _ <| L.toHomeomorph.image_connectedComponentIn hx)
_ = L '' (convexHull ℝ (connectedComponentIn s x)) := (.symm <| L.toAffineMap.image_convexHull _)
_ = univ := by rw [h x hx, image_univ, L.surjective.range_eq]
