English
If f is strictly monotone, then applying f to all elements of two finite sets s and t preserves the colex order between their images exactly when the original sets are ordered dually by colex: toColex(s.image f) ≤ toColex(t.image f) iff toColex s ≤ toColex t.
Русский
Если f строго возрастает, то колексный порядок между образами множества противостоящих множеств s и t сохраняется: toColex(s.image f) ≤ toColex(t.image f) тогда и только тогда, когда toColex s ≤ toColex t.
LaTeX
$$$\text{StrictMono}(f) \Rightarrow toColex\,(s.image\,f) \le toColex\,(t.image\,f) \;\Leftrightarrow\; toColex\,s \le toColex\,t.$$$
Lean4
/-- Strictly monotone functions preserve the colex ordering. -/
theorem toColex_image_le_toColex_image (hf : StrictMono f) :
toColex (s.image f) ≤ toColex (t.image f) ↔ toColex s ≤ toColex t := by
simp [toColex_le_toColex, hf.le_iff_le, hf.injective.eq_iff]
