extChartAt_target_mem_nhds' — Mathlib

English

If I is boundaryless, then for every point y in the target of extChartAt I x, the target is a neighborhood of y.

Русский

Пусть I не имеет границы. Тогда для любого y ∈ (extChartAt I x).target множество extChartAt I x .target является окрестностью y.

LaTeX

$$$\\forall y \\in (extChartAt I x).target:\\; (extChartAt I x).target \\in \\mathcal{N}(y). $$$

Lean4

/-- If we're boundaryless, `(extChartAt I x).target` is a neighborhood of any of its points -/
theorem extChartAt_target_mem_nhds' [I.Boundaryless] {x : M} {y : E} (m : y ∈ (extChartAt I x).target) :
    (extChartAt I x).target ∈ 𝓝 y :=
  (isOpen_extChartAt_target x).mem_nhds m

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