Port from [mathlib3#18375](https://github.com/leanprover-community/mathlib3/pull/18375). It is also possible to define 'length' using Hausdorff measure, [zulipchat](https://leanprover.zulipchat.com/#narrow/channel/217875-Is-there-code-for-X.3F/topic/'length'.20in.20topology/with/556897651).