mem_nhdsWithin_subtype — Mathlib

English

For a subtype a = ⟨x, x ∈ s⟩, the nhdsWithin a t equals the comap under the inclusion map of the nhds of a in α restricted to the image of t.

Русский

Для подтипа a = ⟨x, x ∈ s⟩ окружность nhdsWithin a t равна отображению обратной проекции через вложение к окружности α, ограниченной образом t.

LaTeX

$$$ 𝓝 [t] a = \mathrm{comap}((\uparrow) : s \to α) (𝓝[(\uparrow) '' t] a) $$$

Lean4

theorem mem_nhdsWithin_subtype {s : Set α} {a : { x // x ∈ s }} {t u : Set { x // x ∈ s }} :
    t ∈ 𝓝[u] a ↔ t ∈ comap ((↑) : s → α) (𝓝[(↑) '' u] a) := by
  rw [nhdsWithin, nhds_subtype, principal_subtype, ← comap_inf, ← nhdsWithin]

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