uniqueMDiffWithinAt_univ — Mathlib

English

For any model with corners I on space M, at every x ∈ M the set-univ has the UniqueMDiffWithinAt property.

Русский

Для любой модели I с краями на пространстве M у каждой точки x ∈ M выполняется свойство UniqueMDiffWithinAt для всего множества.

LaTeX

$$$\forall x\in M,\; UniqueMDiffWithinAt I (univ : Set M) x$$$

Lean4

theorem uniqueMDiffWithinAt_univ : UniqueMDiffWithinAt I univ x :=
  by
  unfold UniqueMDiffWithinAt
  simp only [preimage_univ, univ_inter]
  exact I.uniqueDiffOn _ (mem_range_self _)

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