mathlib3

0ed6f7c0 - feat(data/real/liouville, topology/metric_space/basic): further preparations for Liouville (#6201)

feat(data/real/liouville, topology/metric_space/basic): further preparations for Liouville (#6201) These lemmas are used to show that a Liouville number is transcendental. The statement that Liouville numbers are transcendental is the next PR in this sequence! Co-authored-by: Jujian Zhang <jujian.zhang1998@outlook.com>