α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : RegularSpace α
a : α
s : Set α
inst✝ : TopologicalSpace β
f : β → α
hf : Inducing f
b : β
⊢ HasBasis (comap f (𝓝 (f b))) (?m.154015 hf b) (?m.154016 hf b)

α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : RegularSpace α
a : α
s : Set α
⊢ [inst : TopologicalSpace β] → {f : β → α} → Inducing f → β → Sort ?u.153945

α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : RegularSpace α
a : α
s : Set α
⊢ [inst : TopologicalSpace β] → {f : β → α} → (hf : Inducing f) → (a : β) → ?m.154014 hf a → Prop

α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : RegularSpace α
a : α
s : Set α
⊢ [inst : TopologicalSpace β] → {f : β → α} → (hf : Inducing f) → (a : β) → ?m.154014 hf a → Set β
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : RegularSpace α
a : α
s : Set α
inst✝ : TopologicalSpace β
f : β → α
hf : Inducing f
b : β
⊢ HasBasis (𝓝 b) (?m.154015 hf b) (?m.154016 hf b)
rw [hf.nhds_eq_comap b]
no goals
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : RegularSpace α
a : α
s : Set α
inst✝ : TopologicalSpace β
f : β → α
hf : Inducing f
b : β
⊢ HasBasis (comap f (𝓝 (f b))) (?m.154015 hf b) (?m.154016 hf b)

α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : RegularSpace α
a : α
s : Set α
⊢ [inst : TopologicalSpace β] → {f : β → α} → Inducing f → β → Sort ?u.153945

α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : RegularSpace α
a : α
s : Set α
⊢ [inst : TopologicalSpace β] → {f : β → α} → (hf : Inducing f) → (a : β) → ?m.154014 hf a → Prop

α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : RegularSpace α
a : α
s : Set α
⊢ [inst : TopologicalSpace β] → {f : β → α} → (hf : Inducing f) → (a : β) → ?m.154014 hf a → Set β
exact (closed_nhds_basis _).comap _
no goals
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : RegularSpace α
a : α
s✝ : Set α
inst✝ : TopologicalSpace β
f : β → α
hf : Inducing f
b : β
s : Set α
hs : s ∈ 𝓝 (f b) ∧ IsClosed s
⊢ IsClosed (f ⁻¹' id s)
exact hs.2.preimage hf.continuous