range_mem_nhds_isInteriorPoint — Mathlib

English

If x is an interior point, then the image range I is a neighborhood of extChartAt I x x.

Русский

Если x — внутренняя точка, то образ range I является окрестностью extChartAt I x x.

LaTeX

$$$$ I.IsInteriorPoint x \Rightarrow range I \in 𝓝 (extChartAt I x x) $$$$

Lean4

theorem _root_.range_mem_nhds_isInteriorPoint {x : M} (h : I.IsInteriorPoint x) : range I ∈ 𝓝 (extChartAt I x x) :=
  by
  rw [mem_nhds_iff]
  exact ⟨interior (range I), interior_subset, isOpen_interior, h⟩

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