[STATEMENT]
lemma to_Gromov_completion_continuous:
  "continuous_on UNIV to_Gromov_completion"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous_on UNIV to_Gromov_completion
[PROOF STEP]
by (rule homeomorphism_on_continuous[OF to_Gromov_completion_homeomorphism])