uniqueDiffOn_preimage_source — Mathlib

English

For an open family e, the set I^{-1}(e.source) ∩ range(I) has UniqueDiffOn.

Русский

Для открытого источника e.source множества I^{-1}(e.source) ∩ range(I) имеет уникальную дифференцируемость.

LaTeX

$$UniqueDiffOn 𝕜 (I.symm ⁻¹' e.source ∩ range I)$$

Lean4

theorem uniqueDiffOn_preimage_source {β : Type*} [TopologicalSpace β] {e : OpenPartialHomeomorph H β} :
    UniqueDiffOn 𝕜 (I.symm ⁻¹' e.source ∩ range I) :=
  I.uniqueDiffOn_preimage e.open_source

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