English
If s is convex and f is linear, then the preimage under f is convex.
Русский
Если s выпукло и f линейно, то предобраз f^{-1}(s) выпукл.
LaTeX
$$$\Convex 𝕜 s \to \forall f, \Convex 𝕜 (Set.preimage (LinearMap.instFunLike.coe f) s)$$$
Lean4
theorem is_linear_preimage {𝕜₁ : Type*} [Semiring 𝕜₁] [Module 𝕜₁ E] [Module 𝕜₁ F] {s : Set F} [SMul 𝕜 𝕜₁]
[IsScalarTower 𝕜 𝕜₁ E] [IsScalarTower 𝕜 𝕜₁ F] (hs : Convex 𝕜 s) {f : E → F} (hf : IsLinearMap 𝕜₁ f) :
Convex 𝕜 (f ⁻¹' s) :=
hs.linear_preimage <| hf.mk' f