α : Type u
β : Type v
ι : Type ?u.149230
π : ι → Type ?u.149235
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s t : Set α
inst✝ : LocallyCompactSpace β
f : α → β
hf : ClosedEmbedding f
x : α
⊢ HasBasis (𝓝 x) (fun s => s ∈ 𝓝 (f x) ∧ IsCompact s) fun s => f ⁻¹' s
α : Type u
β : Type v
ι : Type ?u.149230
π : ι → Type ?u.149235
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s t : Set α
inst✝ : LocallyCompactSpace β
f : α → β
hf : ClosedEmbedding f
⊢ ∀ (x : α), HasBasis (𝓝 x) (fun s => s ∈ 𝓝 (f x) ∧ IsCompact s) fun s => f ⁻¹' s
intro x
α : Type u
β : Type v
ι : Type ?u.149230
π : ι → Type ?u.149235
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s t : Set α
inst✝ : LocallyCompactSpace β
f : α → β
hf : ClosedEmbedding f
x : α
⊢ HasBasis (comap f (𝓝 (f x))) (fun s => s ∈ 𝓝 (f x) ∧ IsCompact s) fun s => f ⁻¹' s
α : Type u
β : Type v
ι : Type ?u.149230
π : ι → Type ?u.149235
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s t : Set α
inst✝ : LocallyCompactSpace β
f : α → β
hf : ClosedEmbedding f
x : α
⊢ HasBasis (𝓝 x) (fun s => s ∈ 𝓝 (f x) ∧ IsCompact s) fun s => f ⁻¹' s
rw [hf.toInducing.nhds_eq_comap]
no goals
α : Type u
β : Type v
ι : Type ?u.149230
π : ι → Type ?u.149235
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s t : Set α
inst✝ : LocallyCompactSpace β
f : α → β
hf : ClosedEmbedding f
x : α
⊢ HasBasis (comap f (𝓝 (f x))) (fun s => s ∈ 𝓝 (f x) ∧ IsCompact s) fun s => f ⁻¹' s
exact (compact_basis_nhds _).comap _