affine_preimage — Mathlib

English

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

Русский

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

LaTeX

$$$$ \\operatorname{Convex}_{\\mathbb{K}}\\bigl( f^{-1}(s) \\bigr) $$$$

Lean4

/-- The preimage of a convex set under an affine map is convex. -/
theorem affine_preimage (f : E →ᵃ[𝕜] F) {s : Set F} (hs : Convex 𝕜 s) : Convex 𝕜 (f ⁻¹' s) := fun _ hx =>
  (hs hx).affine_preimage _

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