preimage_nhds_within_coinduced — Mathlib

English

If a ∈ t, t is open, and s is a neighborhood of X(a) in the coinduced topology via X, then X^{-1}(s) is a neighborhood of a.

Русский

Если a ∈ t, t открыто и s — окрестность X(a) в коиндуктивной топологии через X, то X^{-1}(s) является окрестностью a.

LaTeX

$$$ a \in t \land IsOpen t \land s \in @nhds β (.coinduced (fun x : t => X x) inferInstance) (X a) \Rightarrow X^{-1}(s) \in \mathcal{N} a $$$

Lean4

theorem preimage_nhds_within_coinduced {X : α → β} {s : Set β} {t : Set α} {a : α} (h : a ∈ t) (ht : IsOpen t)
    (hs : s ∈ @nhds β (.coinduced (fun x : t => X x) inferInstance) (X a)) : X ⁻¹' s ∈ 𝓝 a :=
  by
  rw [← ht.nhdsWithin_eq h]
  exact preimage_nhdsWithin_coinduced' h hs

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