uniqueDiffOn_image — Mathlib

English

For a continuous linear equivalence e, UniqueDiffOn 𝕜 (image e s) iff UniqueDiffOn 𝕜 s.

Русский

Для эквивиалентности e выполняется: UniqueDiffOn 𝕜 (image e s) эквивалентно UniqueDiffOn 𝕜 s.

LaTeX

$$$$ \\text{UniqueDiffOn } 𝕜 (\\text{image } e\\ s) \\iff \\text{UniqueDiffOn } 𝕜 s $$$$

Lean4

theorem uniqueDiffOn_image (e : E ≃L[𝕜] F) (h : UniqueDiffOn 𝕜 s) : UniqueDiffOn 𝕜 (e '' s) :=
  h.image (fun _ _ => e.hasFDerivWithinAt) fun _ _ => e.surjective.denseRange

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