α : Type u
β : Type v
ι : Type ?u.150029
π : ι → Type ?u.150034
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s t : Set α
inst✝ : LocallyCompactSpace β
f : α → β
hf : OpenEmbedding f
this : ∀ (x : α), HasBasis (𝓝 x) (fun s => (s ∈ 𝓝 (f x) ∧ IsCompact s) ∧ s ⊆ range f) fun s => f ⁻¹' s
⊢ LocallyCompactSpace α
α : Type u
β : Type v
ι : Type ?u.150029
π : ι → Type ?u.150034
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s t : Set α
inst✝ : LocallyCompactSpace β
f : α → β
hf : OpenEmbedding f
⊢ LocallyCompactSpace α
have : ∀ x : α, (𝓝 x).HasBasis
    (fun s => (s ∈ 𝓝 (f x) ∧ IsCompact s) ∧ s ⊆ range f) fun s => f ⁻¹' s := by
  intro x
  rw [hf.toInducing.nhds_eq_comap]
  exact
    ((compact_basis_nhds _).restrict_subset <| hf.open_range.mem_nhds <| mem_range_self _).comap _
α : Type u
β : Type v
ι : Type ?u.150029
π : ι → Type ?u.150034
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s✝ t : Set α
inst✝ : LocallyCompactSpace β
f : α → β
hf : OpenEmbedding f
this : ∀ (x : α), HasBasis (𝓝 x) (fun s => (s ∈ 𝓝 (f x) ∧ IsCompact s) ∧ s ⊆ range f) fun s => f ⁻¹' s
x : α
s : Set β
hs : (s ∈ 𝓝 (f x) ∧ IsCompact s) ∧ s ⊆ range f
⊢ IsCompact (f ⁻¹' s)
α : Type u
β : Type v
ι : Type ?u.150029
π : ι → Type ?u.150034
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s t : Set α
inst✝ : LocallyCompactSpace β
f : α → β
hf : OpenEmbedding f
this : ∀ (x : α), HasBasis (𝓝 x) (fun s => (s ∈ 𝓝 (f x) ∧ IsCompact s) ∧ s ⊆ range f) fun s => f ⁻¹' s
⊢ LocallyCompactSpace α
refine' locallyCompactSpace_of_hasBasis this fun x s hs => _
α : Type u
β : Type v
ι : Type ?u.150029
π : ι → Type ?u.150034
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s✝ t : Set α
inst✝ : LocallyCompactSpace β
f : α → β
hf : OpenEmbedding f
this : ∀ (x : α), HasBasis (𝓝 x) (fun s => (s ∈ 𝓝 (f x) ∧ IsCompact s) ∧ s ⊆ range f) fun s => f ⁻¹' s
x : α
s : Set β
hs : (s ∈ 𝓝 (f x) ∧ IsCompact s) ∧ s ⊆ range f
⊢ IsCompact s
α : Type u
β : Type v
ι : Type ?u.150029
π : ι → Type ?u.150034
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s✝ t : Set α
inst✝ : LocallyCompactSpace β
f : α → β
hf : OpenEmbedding f
this : ∀ (x : α), HasBasis (𝓝 x) (fun s => (s ∈ 𝓝 (f x) ∧ IsCompact s) ∧ s ⊆ range f) fun s => f ⁻¹' s
x : α
s : Set β
hs : (s ∈ 𝓝 (f x) ∧ IsCompact s) ∧ s ⊆ range f
⊢ IsCompact (f ⁻¹' s)
rw [← hf.toInducing.isCompact_iff, image_preimage_eq_of_subset hs.2]
no goals
α : Type u
β : Type v
ι : Type ?u.150029
π : ι → Type ?u.150034
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s✝ t : Set α
inst✝ : LocallyCompactSpace β
f : α → β
hf : OpenEmbedding f
this : ∀ (x : α), HasBasis (𝓝 x) (fun s => (s ∈ 𝓝 (f x) ∧ IsCompact s) ∧ s ⊆ range f) fun s => f ⁻¹' s
x : α
s : Set β
hs : (s ∈ 𝓝 (f x) ∧ IsCompact s) ∧ s ⊆ range f
⊢ IsCompact s
exact hs.1.2
α : Type u
β : Type v
ι : Type ?u.150029
π : ι → Type ?u.150034
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s t : Set α
inst✝ : LocallyCompactSpace β
f : α → β
hf : OpenEmbedding f
x : α
⊢ HasBasis (𝓝 x) (fun s => (s ∈ 𝓝 (f x) ∧ IsCompact s) ∧ s ⊆ range f) fun s => f ⁻¹' s
α : Type u
β : Type v
ι : Type ?u.150029
π : ι → Type ?u.150034
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s t : Set α
inst✝ : LocallyCompactSpace β
f : α → β
hf : OpenEmbedding f
⊢ ∀ (x : α), HasBasis (𝓝 x) (fun s => (s ∈ 𝓝 (f x) ∧ IsCompact s) ∧ s ⊆ range f) fun s => f ⁻¹' s
intro x
α : Type u
β : Type v
ι : Type ?u.150029
π : ι → Type ?u.150034
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s t : Set α
inst✝ : LocallyCompactSpace β
f : α → β
hf : OpenEmbedding f
x : α
⊢ HasBasis (comap f (𝓝 (f x))) (fun s => (s ∈ 𝓝 (f x) ∧ IsCompact s) ∧ s ⊆ range f) fun s => f ⁻¹' s
α : Type u
β : Type v
ι : Type ?u.150029
π : ι → Type ?u.150034
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s t : Set α
inst✝ : LocallyCompactSpace β
f : α → β
hf : OpenEmbedding f
x : α
⊢ HasBasis (𝓝 x) (fun s => (s ∈ 𝓝 (f x) ∧ IsCompact s) ∧ s ⊆ range f) fun s => f ⁻¹' s
rw [hf.toInducing.nhds_eq_comap]
no goals
α : Type u
β : Type v
ι : Type ?u.150029
π : ι → Type ?u.150034
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s t : Set α
inst✝ : LocallyCompactSpace β
f : α → β
hf : OpenEmbedding f
x : α
⊢ HasBasis (comap f (𝓝 (f x))) (fun s => (s ∈ 𝓝 (f x) ∧ IsCompact s) ∧ s ⊆ range f) fun s => f ⁻¹' s
exact
  ((compact_basis_nhds _).restrict_subset <| hf.open_range.mem_nhds <| mem_range_self _).comap _