α : Type u
β✝ : Type v
γ : Type ?u.159970
δ : Type ?u.159973
ε : Type ?u.159976
ζ : Type ?u.159979
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β✝
inst✝ : TopologicalSpace γ
p✝ : α → Prop
β : Type u_1
p : α → Prop
b : Filter β
f : β → Subtype p
a : α
ha : p a
⊢ Tendsto (Subtype.val ∘ f) b (𝓝 a) ↔ Tendsto (fun x => ↑(f x)) b (𝓝 ↑{ val := a, property := ha })
α : Type u
β✝ : Type v
γ : Type ?u.159970
δ : Type ?u.159973
ε : Type ?u.159976
ζ : Type ?u.159979
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β✝
inst✝ : TopologicalSpace γ
p✝ : α → Prop
β : Type u_1
p : α → Prop
b : Filter β
f : β → Subtype p
a : α
ha : p a
⊢ Tendsto f b (𝓝 { val := a, property := ha }) ↔ Tendsto (fun x => ↑(f x)) b (𝓝 ↑{ val := a, property := ha })
rw [nhds_subtype_eq_comap, tendsto_comap_iff]
no goals
α : Type u
β✝ : Type v
γ : Type ?u.159970
δ : Type ?u.159973
ε : Type ?u.159976
ζ : Type ?u.159979
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β✝
inst✝ : TopologicalSpace γ
p✝ : α → Prop
β : Type u_1
p : α → Prop
b : Filter β
f : β → Subtype p
a : α
ha : p a
⊢ Tendsto (Subtype.val ∘ f) b (𝓝 a) ↔ Tendsto (fun x => ↑(f x)) b (𝓝 ↑{ val := a, property := ha })
rfl