α : Type u_2
β : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s✝ : Set β
ι : Type ?u.194
U : ι → Opens β
hU : iSup U = ⊤
s : Set β
h : ∀ (a : α), 𝓝 a = comap f (𝓝 (f a))
⊢ ∀ (a : ↑(f ⁻¹' s)), 𝓝 a = comap Subtype.val (comap f (𝓝 (f ↑a)))
α : Type u_2
β : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s✝ : Set β
ι : Type ?u.194
U : ι → Opens β
hU : iSup U = ⊤
s : Set β
h : Inducing f
⊢ Inducing (restrictPreimage s f)
simp_rw [inducing_subtype_val.inducing_iff, inducing_iff_nhds, restrictPreimage,
  MapsTo.coe_restrict, restrict_eq, ← @Filter.comap_comap _ _ _ _ _ f, Function.comp_apply] at h⊢
α : Type u_2
β : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s✝ : Set β
ι : Type ?u.194
U : ι → Opens β
hU : iSup U = ⊤
s : Set β
h : ∀ (a : α), 𝓝 a = comap f (𝓝 (f a))
a : ↑(f ⁻¹' s)
⊢ 𝓝 a = comap Subtype.val (comap f (𝓝 (f ↑a)))
α : Type u_2
β : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s✝ : Set β
ι : Type ?u.194
U : ι → Opens β
hU : iSup U = ⊤
s : Set β
h : ∀ (a : α), 𝓝 a = comap f (𝓝 (f a))
⊢ ∀ (a : ↑(f ⁻¹' s)), 𝓝 a = comap Subtype.val (comap f (𝓝 (f ↑a)))
intro a
no goals
α : Type u_2
β : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s✝ : Set β
ι : Type ?u.194
U : ι → Opens β
hU : iSup U = ⊤
s : Set β
h : ∀ (a : α), 𝓝 a = comap f (𝓝 (f a))
a : ↑(f ⁻¹' s)
⊢ 𝓝 a = comap Subtype.val (comap f (𝓝 (f ↑a)))
rw [← h, ← inducing_subtype_val.nhds_eq_comap]