case a
α : Type u
β : Type v
γ : Type ?u.44623
f✝ : α → β
ι : Sort ?u.44630
T : TopologicalSpace α
f : β → α
a : β
s : Set β
⊢ s ∈ 𝓝 a ↔ s ∈ comap f (𝓝 (f a))
α : Type u
β : Type v
γ : Type ?u.44623
f✝ : α → β
ι : Sort ?u.44630
T : TopologicalSpace α
f : β → α
a : β
⊢ 𝓝 a = comap f (𝓝 (f a))
ext s
no goals
case a
α : Type u
β : Type v
γ : Type ?u.44623
f✝ : α → β
ι : Sort ?u.44630
T : TopologicalSpace α
f : β → α
a : β
s : Set β
⊢ s ∈ 𝓝 a ↔ s ∈ comap f (𝓝 (f a))
rw [mem_nhds_induced, mem_comap]