extend_source_mem_nhdsWithin — Mathlib

English

If x ∈ f.source, then the extended source is a neighborhood of x relative to s.

Русский

Если x ∈ f.source, то расширенная область источника является окрестностью x внутри s.

LaTeX

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

Lean4

theorem extend_source_mem_nhdsWithin {x : M} (h : x ∈ f.source) : (f.extend I).source ∈ 𝓝[s] x :=
  mem_nhdsWithin_of_mem_nhds <| extend_source_mem_nhds f h

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