strictConvex_preimage — Mathlib

English

For a linear isomorphism e, a set s has strict convexity if and only if its preimage under e is strictly convex: StrictConvex 𝕜 (e⁻¹' s) iff StrictConvex 𝕜 s.

Русский

Пусть e — линейное изоморфизм, тогда множество имеет строгую выпуклость тогда и только тогда, когда его образ/обратно прообраз сохраняют строгую выпуклость: StrictConvex 𝕜 (e⁻¹' s) ⇔ StrictConvex 𝕜 s.

LaTeX

$$$$\\text{StrictConvex}_{\\mathbb{K}}(e^{-1}(s)) \\iff \\text{StrictConvex}_{\\mathbb{K}}(s).$$$$

Lean4

@[simp]
theorem strictConvex_preimage {s : Set F} (e : E ≃L[𝕜] F) : StrictConvex 𝕜 (e ⁻¹' s) ↔ StrictConvex 𝕜 s :=
  ⟨fun h ↦
    Function.LeftInverse.preimage_preimage e.right_inv s ▸
      h.linear_preimage e.symm.toLinearMap e.symm.continuous e.symm.injective,
    fun h ↦ h.linear_preimage e.toLinearMap e.continuous e.injective⟩

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