affine_image — Mathlib

English

The image of a convex set under an affine map is convex.

Русский

Образ выпуклого множества под аффинным отображением выпукл.

LaTeX

$$$$ \\operatorname{Convex}_{\\mathbb{K}}\\bigl( f\\,' s \\bigr) $$$$

Lean4

/-- The image of a convex set under an affine map is convex. -/
theorem affine_image (f : E →ᵃ[𝕜] F) (hs : Convex 𝕜 s) : Convex 𝕜 (f '' s) :=
  by
  rintro _ ⟨x, hx, rfl⟩
  exact (hs hx).affine_image _

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