English
If f is strictly monotone, then the map s ↦ toColex(s.image f) is strictly monotone with respect to the colex order: s < t in Colex implies toColex(s.image f) < toColex(t.image f).
Русский
Если f строго монотонна, отображение s ↦ toColex(s.image f) сохраняет строгий порядок колекс: s < t в Colex тогда и только если toColex(s.image f) < toColex(t.image f).
LaTeX
$$$\text{StrictMono}(f) \Rightarrow (\forall s,t,\ s <_{Colex} t \Rightarrow toColex\,(s.image\,f) < toColex\,(t.image\,f)).$$$
Lean4
/-- Strictly monotone functions preserve the colex ordering. -/
theorem toColex_image_lt_toColex_image (hf : StrictMono f) :
toColex (s.image f) < toColex (t.image f) ↔ toColex s < toColex t :=
lt_iff_lt_of_le_iff_le <| toColex_image_le_toColex_image hf