Mathport failing on LittleO and BigO

Stream: mathlib4

[Moritz Doll]

I don't know whether this has been noted before, but mathport seems to ignore the aligns for IsLittleO and IsBigO. I don't know what causes this, but it is a bit annoying in !4#4132 and will probably only become more annoying with more analysis.

[Jireh Loreaux]

Have you checked mathport to make sure they aren't dubious translations? I ported asymptotics and I don't recall them being dubious, but if they were that could explain it, I think.