chartAt_inclusion_symm_eventuallyEq

English

If e is as above and e' lies in the singleton chart atlas, then e' equals e.

Русский

Если e' лежит в атласе единичного чарта, то он равен e.

LaTeX

$$singletonChartedSpace_mem_atlas_eq$$

Lean4

theorem chartAt_inclusion_symm_eventuallyEq {U V : Opens M} (hUV : U ≤ V) {x : U} :
    (chartAt H (Opens.inclusion hUV x)).symm =ᶠ[𝓝 (chartAt H (Opens.inclusion hUV x) (Set.inclusion hUV x))]
      Opens.inclusion hUV ∘ (chartAt H x).symm :=
  by
  set e := chartAt H (x : M)
  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_of_le ⟨x⟩ ⟨Opens.inclusion hUV x⟩ hUV

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