is_linear_preimage — Mathlib

English

If s is strictly convex and f is an injective continuous linear map, then the preimage is strictly convex.

Русский

Если s строго выпукло и f инъективно и непрерывно линейно, то прообраз строго выпукл.

LaTeX

$$$StrictConvex 𝕜 s \Rightarrow \forall {f : E \to F}, IsLinearMap 𝕜 f \Rightarrow Continuous f \Rightarrow Injective f \Rightarrow StrictConvex 𝕜 (Set.preimage f s)$$$

Lean4

theorem is_linear_preimage {s : Set F} (hs : StrictConvex 𝕜 s) {f : E → F} (h : IsLinearMap 𝕜 f) (hf : Continuous f)
    (hfinj : Injective f) : StrictConvex 𝕜 (s.preimage f) :=
  hs.linear_preimage (h.mk' f) hf hfinj

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