α : Type u
β : Type v
X : Type ?u.547230
ι : Type ?u.547233
inst✝ : PseudoMetricSpace α
f : β → α
l : Filter β
x : α
h : Tendsto (fun y => dist (f y) x) l atTop
⊢ Tendsto f l (comap (fun y => dist y x) atTop)
α : Type u
β : Type v
X : Type ?u.547230
ι : Type ?u.547233
inst✝ : PseudoMetricSpace α
f : β → α
l : Filter β
x : α
h : Tendsto (fun y => dist (f y) x) l atTop
⊢ Tendsto f l (cocompact α)
refine' Tendsto.mono_right _ (comap_dist_right_atTop_le_cocompact x)
no goals
α : Type u
β : Type v
X : Type ?u.547230
ι : Type ?u.547233
inst✝ : PseudoMetricSpace α
f : β → α
l : Filter β
x : α
h : Tendsto (fun y => dist (f y) x) l atTop
⊢ Tendsto f l (comap (fun y => dist y x) atTop)
rwa [tendsto_comap_iff]