preimage_coe_mem_nhds_subtype — Mathlib

English

For a subtype a with a representative a from s, the preimage of t under the coercion map belongs to nhds a iff t ∈ nhdsWithin s (↑a).

Русский

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

LaTeX

$$$ (↑)^{-1}' t ∈ 𝓝 a \iff t ∈ 𝓝[s] (↑a) $$$

Lean4

theorem preimage_coe_mem_nhds_subtype {s t : Set α} {a : s} : (↑) ⁻¹' t ∈ 𝓝 a ↔ t ∈ 𝓝[s] ↑a := by
  rw [← map_nhds_subtype_val, mem_map]

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