chartAt_subtype_val_symm_eventuallyEq

English

Each chart of a charted space yields a Structomorph between the corresponding subtype charts.

Русский

Каждый чарт чартизированного пространства порождает Structomorph между соответствующими чартами-подтипами.

LaTeX

$$OpenPartialHomeomorph.toStructomorph$$

Lean4

theorem chartAt_subtype_val_symm_eventuallyEq (U : Opens M) {x : U} :
    (chartAt H x.val).symm =ᶠ[𝓝 (chartAt H x.val x.val)] Subtype.val ∘ (chartAt H x).symm :=
  by
  set e := chartAt H x.val
  have heUx_nhds : (e.subtypeRestr ⟨x⟩).target ∈ 𝓝 (e x) :=
    by
    apply (e.subtypeRestr ⟨x⟩).open_target.mem_nhds
    exact e.map_subtype_source ⟨x⟩ (mem_chart_source _ _)
  exact Filter.eventuallyEq_of_mem heUx_nhds (e.subtypeRestr_symm_eqOn ⟨x⟩)

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