α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
s : Set α
l : Filter β
f✝ : α → β
f : β → ↑(Iio a)
⊢ Tendsto (Subtype.val ∘ f) l (𝓝[Iio a] a) ↔ Tendsto (fun x => ↑(f x)) l (𝓝[Iio a] a)
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
s : Set α
l : Filter β
f✝ : α → β
f : β → ↑(Iio a)
⊢ Tendsto f l atTop ↔ Tendsto (fun x => ↑(f x)) l (𝓝[Iio a] a)
rw [← comap_coe_Iio_nhdsWithin_Iio, tendsto_comap_iff]
no goals
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
s : Set α
l : Filter β
f✝ : α → β
f : β → ↑(Iio a)
⊢ Tendsto (Subtype.val ∘ f) l (𝓝[Iio a] a) ↔ Tendsto (fun x => ↑(f x)) l (𝓝[Iio a] a)
rfl