rewrite [← isLittleO_map, map_fst_prod]
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝⁵ : NormedAddCommGroup α
inst✝⁴ : LinearOrder α
inst✝³ : ProperSpace α
inst✝² : NormedAddCommGroup F
inst✝¹ : NoMaxOrder α
inst✝ : ClosedIciTopology α
c : F
ly : Filter E
x✝ : ly.NeBot
⊢ ((fun x => c) ∘ Prod.fst) =o[atTop ×ˢ ly] (id ∘ Prod.fst)
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝⁵ : NormedAddCommGroup α
inst✝⁴ : LinearOrder α
inst✝³ : ProperSpace α
inst✝² : NormedAddCommGroup F
inst✝¹ : NoMaxOrder α
inst✝ : ClosedIciTopology α
c : F
ly : Filter E
x✝ : ly.NeBot
⊢ (fun x => c) =o[atTop] id