α : Type u
β : Type v
γ : Type w
δ : Type ?u.311794
ι : Sort x
m : α → β
f : Filter α
g : Filter β
i : γ → α
h : range i ∈ f
⊢ (map m ∘ map i) (comap i f) ≤ g ↔ Tendsto m f g
α : Type u
β : Type v
γ : Type w
δ : Type ?u.311794
ι : Sort x
m : α → β
f : Filter α
g : Filter β
i : γ → α
h : range i ∈ f
⊢ Tendsto (m ∘ i) (comap i f) g ↔ Tendsto m f g
rw [Tendsto, ← map_compose]