image — Mathlib

English

If e is a continuous linear equivalence, then UniqueDiffOn 𝕜 s implies UniqueDiffOn 𝕜 (e''s).

Русский

Если e — непрерывная линейная эквив, то UniqueDiffOn 𝕜 s влечет UniqueDiffOn 𝕜 (e''s).

LaTeX

$$$$ \\text{UniqueDiffOn } 𝕜 s \\Rightarrow \\text{UniqueDiffOn } 𝕜 (e''s) $$$$

Lean4

theorem image {f' : E → E →L[𝕜] F} (hs : UniqueDiffOn 𝕜 s) (hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x)
    (hd : ∀ x ∈ s, DenseRange (f' x)) : UniqueDiffOn 𝕜 (f '' s) :=
  forall_mem_image.2 fun x hx => (hf' x hx).uniqueDiffWithinAt (hs x hx) (hd x hx)

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