rewrite [← isLittleO_map, map_snd_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✝¹ : NoMinOrder α
inst✝ : ClosedIicTopology α
c : F
lx : Filter E
x✝ : lx.NeBot
⊢ ((fun x => c) ∘ Prod.snd) =o[lx ×ˢ atBot] (id ∘ Prod.snd)
α : 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✝¹ : NoMinOrder α
inst✝ : ClosedIicTopology α
c : F
lx : Filter E
x✝ : lx.NeBot
⊢ (fun x => c) =o[atBot] id