mem_nhds_subtype — Mathlib

English

For a subset s of X and x in the subtype {x ∈ s}, and t ⊆ the subtype, t ∈ 𝓝 x iff there exists u ∈ 𝓝 (x ∈ X) with Subtype.val^{-1}(u) ⊆ t.

Русский

Для подмножества s ⊆ X и x ∈ {x ∈ s}, t ⊆ подтип, t ∈ 𝓝 x тогда и только тогда, когда существует u ∈ 𝓝 (x ∈ X) с обратной проекцией Subtype.val(u) ⊆ t.

LaTeX

$$$ t \\in 𝓝 x \\iff \\exists u \\in 𝓝 (x), (\\mathrm{Subtype}.val)^{-1}(u) \\subseteq t. $$$

Lean4

theorem mem_nhds_subtype (s : Set X) (x : { x // x ∈ s }) (t : Set { x // x ∈ s }) :
    t ∈ 𝓝 x ↔ ∃ u ∈ 𝓝 (x : X), Subtype.val ⁻¹' u ⊆ t :=
  mem_nhds_induced _ x t

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