chart_eq — Mathlib

English

If s is nonempty and e belongs to atlas H s, there exists x ∈ s such that e = chartAt H (x).subtypeRestr.

Русский

Если s непусто и e принадлежит atlas H s, существует x ∈ s такого что e = chartAt H (x).subtypeRestr.

LaTeX

$$chart_eq$$

Lean4

/-- If `s` is a non-empty open subset of `M`, every chart of `s` is the restriction
of some chart on `M`. -/
theorem chart_eq {s : Opens M} (hs : Nonempty s) {e : OpenPartialHomeomorph s H} (he : e ∈ atlas H s) :
    ∃ x : s, e = (chartAt H (x : M)).subtypeRestr hs :=
  by
  rcases he with ⟨xset, ⟨x, hx⟩, he⟩
  exact ⟨x, mem_singleton_iff.mp (by convert he)⟩

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