extChartAt_source_mem_nhdsWithin'

English

The source of extChartAt I x lies in nhdsWithin x with respect to an arbitrary subset s.

Русский

Источник extChartAt I x лежит в nhdsWithin x относительно произвольного множества s.

LaTeX

$$$ (extChartAt I x).source \\in 𝓝[s] x$$$

Lean4

theorem extChartAt_source_mem_nhdsWithin' {x x' : M} (h : x' ∈ (extChartAt I x).source) :
    (extChartAt I x).source ∈ 𝓝[s] x' :=
  mem_nhdsWithin_of_mem_nhds (extChartAt_source_mem_nhds' h)

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