mathlib

786a0694 - feat(data/real/basic): inf/sup coincindes with elementwise versions on cauchy sequences