Tightness under forgetting the internal measure

The underlying GH projection is continuous and has compact inverse images of compact sets. Thus a family of measures on GHP space is tight exactly when its underlying GH image is tight. These outer measures may be arbitrary; the compact spaces represented by points of GHP space still carry Borel probability measures on their whole carriers.

theorem BGW.MetricMeasure.MeasuredGHSpace.isTightMeasureSet_map_underlyingGH_iff (S : Set (MeasureTheory.Measure MeasuredGHSpace)) : MeasureTheory.IsTightMeasureSet (MeasureTheory.Measure.map underlyingGH '' S) ↔ MeasureTheory.IsTightMeasureSet S

Tightness of random compact measured spaces is equivalent to tightness after forgetting their internal probability measures. No full-support hypothesis is imposed.