The unit interval inside the nonnegative reals

Two facts about unitInterval.toNNReal : I → ℝ≥0, the inclusion of the unit interval into the nonnegative reals: its values are at most one, and clamping a real t to the unit interval with Set.projIcc and reading it back in ℝ≥0 gives min t.toNNReal 1 (so min t 1 for t : ℝ≥0). They let paths parametrized by the unit interval be reparametrized by a nonnegative time, as in TauCeti.Topology.PathSpace.Moore.Comparison.Basic.

@[simp]

theorem unitInterval.toNNReal_le_one (s : ↑unitInterval) : toNNReal s ≤ 1

The inclusion of the unit interval into ℝ≥0 takes values at most one.

@[simp]

theorem unitInterval.toNNReal_projIcc (t : ℝ) : toNNReal (Set.projIcc 0 1 ⋯ t) = min t.toNNReal 1

Clamping a real t to the unit interval, read back in ℝ≥0, is min t.toNNReal 1.