extend_source_mem_nhds — Mathlib

English

If x ∈ f.source, then the extended source (the domain of f extended by I) forms a neighborhood of x.

Русский

Пусть x принадлежит f.source; тогда расширенная область источника образует окрестность x.

LaTeX

$$$ x \\in f.source \\implies (f \\extend I).source \\in \\mathcal{N}(x). $$$

Lean4

theorem extend_source_mem_nhds {x : M} (h : x ∈ f.source) : (f.extend I).source ∈ 𝓝 x :=
  (isOpen_extend_source f).mem_nhds <| by rwa [f.extend_source]

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