toColex_image_ofColex_strictMono — Mathlib

English

If f is strictly increasing, then the map s ↦ toColex (image f s) preserves the strictness of order in Colex, i.e., the order is monotone with respect to s.

Русский

Если f строго возрастает, то отображение s ↦ toColex image f s сохраняет строгость порядка в Colex; порядок монотонен по отношению к s.

LaTeX

$$$\text{StrictMono}(f) \Rightarrow \text{StrictMono}(\lambda s. toColex\,(s.image\,f)).$$$

Lean4

theorem toColex_image_ofColex_strictMono (hf : StrictMono f) : StrictMono fun s ↦ toColex <| image f <| ofColex s :=
  fun _s _t ↦ (toColex_image_lt_toColex_image hf).2

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