toColex_image_lt_toColex_image — Mathlib

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

Похожие утверждения