English
For a map X : α → β, a subset t of α, a subset s of β, and a point a with a ∈ t, if s is a neighborhood of X(a) in the coinduced topology on β from the map restricted to t, then X^{-1}(s) is a neighborhood of a in 𝓝_t(a).
Русский
Для отображения X: α→β, множества t⊆α, s⊆β и точки a с a∈t, если s является окрестностью X(a) в коиндуктивной топологии β через X, ограниченную до t, то X^{-1}(s) является окрестностью a в 𝓝_t(a).
LaTeX
$$$ X \colon \alpha \to \beta ,\ a \in t ,\ s \in \mathcal{N}^{coinduced}_{X(a)} \bigl(Xa\bigr) \Rightarrow X^{-1}(s) \in \mathcal{N}_t(a) $$$
Lean4
theorem preimage_nhdsWithin_coinduced' {X : α → β} {s : Set β} {t : Set α} {a : α} (h : a ∈ t)
(hs : s ∈ @nhds β (.coinduced (fun x : t => X x) inferInstance) (X a)) : X ⁻¹' s ∈ 𝓝[t] a :=
by
lift a to t using h
replace hs : (fun x : t => X x) ⁻¹' s ∈ 𝓝 a := preimage_nhds_coinduced hs
rwa [← map_nhds_subtype_val, mem_map]
