uniqueDiffOn_image_iff — Mathlib

English

Same as above, with simp lemma assertion for the image-under-equivalence.

Русский

Аналогично, с предпосылкой простоты образа через эквив.

LaTeX

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

Lean4

@[simp]
theorem uniqueDiffOn_image_iff (e : E ≃L[𝕜] F) : UniqueDiffOn 𝕜 (e '' s) ↔ UniqueDiffOn 𝕜 s :=
  ⟨fun h => e.symm_image_image s ▸ e.symm.uniqueDiffOn_image h, e.uniqueDiffOn_image⟩

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