chart_eq' — Mathlib

English

Restricting a chart to its source s yields a chart in the maximal atlas of s.

Русский

Ограничение чарта до источника s дает чарт в максимальном атласе s.

LaTeX

$$e.subtypeRestr hs ∈ G.maximalAtlas s$$

Lean4

/-- If `t` is a non-empty open subset of `H`,
every chart of `t` is the restriction of some chart on `H`. -/
-- XXX: can I unify this with `chart_eq`?

theorem chart_eq' {t : Opens H} (ht : Nonempty t) {e' : OpenPartialHomeomorph t H} (he' : e' ∈ atlas H t) :
    ∃ x : t, e' = (chartAt H ↑x).subtypeRestr ht :=
  chart_eq ht he'

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