uniqueDiffOn_preimage_iff — Mathlib

English

If e is a continuous linear equivalence, UniqueDiffOn 𝕜 (preimage of s under e) iff UniqueDiffOn 𝕜 s.

Русский

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

LaTeX

$$$$ \\text{UniqueDiffOn } 𝕜 (\\text{preimage } (\\text{coe} \\, e) \\, s) \\iff \\text{UniqueDiffOn } 𝕜 s $$$$

Lean4

@[simp]
theorem uniqueDiffOn_preimage_iff (e : F ≃L[𝕜] E) : UniqueDiffOn 𝕜 (e ⁻¹' s) ↔ UniqueDiffOn 𝕜 s := by
  rw [← e.image_symm_eq_preimage, e.symm.uniqueDiffOn_image_iff]

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