is_linear_preimage — Mathlib

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

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