Gromov--Hausdorff compatibility of the coding maps

The forgetful map from rooted measured classes to GH classes sends the class of a coded tree to its GH class. The coding-independent continuity and law-transport API lives in BGW.MetricMeasure.RootedUnderlyingGH and is publicly re-exported here.

Reference: D. Burago, Y. Burago and S. Ivanov, A Course in Metric Geometry, AMS, 2001, Chapter 7.

theorem BGW.ContinuumTrees.Coding.underlyingGH_forgetRoot_rootedMeasuredGHSpace (g : C(↑unitInterval, ℝ)) : forgetToGH (rootedMeasuredGHSpace g) = GromovHausdorff.toGHSpace (Space g)

The GH class of the coded tree is the forgetful image of its rooted measured class.