nhdsWithin_subtype — Mathlib

English

For s ⊆ α and a ∈ s as a subtype, the nhdsWithin t at a equals comap of inclusion from nhdsWithin of a.val in α with image of t.

Русский

Для s ⊆ α и a ∈ s как подтип, окружность nhdsWithin t в a равна обобщённому образу через вложение из nhdsWithin a.val в α образа t.

LaTeX

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

Lean4

theorem nhdsWithin_subtype (s : Set α) (a : { x // x ∈ s }) (t : Set { x // x ∈ s }) :
    𝓝[t] a = comap ((↑) : s → α) (𝓝[(↑) '' t] a) :=
  Filter.ext fun _ => mem_nhdsWithin_subtype

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