linear_preimage — Mathlib

English

If s is convex and f is a linear map, then f^{-1}(s) is convex.

Русский

Если s выпукло и f — линейное отображение, то предобраз f^{-1}(s) выпукл.

LaTeX

$$$\Convex 𝕜 s \to \text{Convex 𝕜} (f^{-1} s)$$$

Lean4

theorem linear_preimage {𝕜₁ : Type*} [Semiring 𝕜₁] [Module 𝕜₁ E] [Module 𝕜₁ F] {s : Set F} [SMul 𝕜 𝕜₁]
    [IsScalarTower 𝕜 𝕜₁ E] [IsScalarTower 𝕜 𝕜₁ F] (hs : Convex 𝕜 s) (f : E →ₗ[𝕜₁] F) : Convex 𝕜 (f ⁻¹' s) :=
  fun x hx y hy a b ha hb hab =>
  by
  rw [mem_preimage, f.map_add, LinearMap.map_smul_of_tower, LinearMap.map_smul_of_tower]
  exact hs hx hy ha hb hab

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