toLex_mono — Mathlib

English

If α is a partial order, then the map toLex: NonemptyInterval α → Lex(NonemptyInterval α) is monotone.

Русский

Если α частично упорядочено, то отображение toLex: NonemptyInterval α → Lex(NonemptyInterval α) монотонно.

LaTeX

$$$ x \le y \Rightarrow toLex(x) \le toLex(y) $$$

Lean4

theorem toLex_mono [PartialOrder α] : Monotone (toLex : NonemptyInterval α → _) :=
  Prod.Lex.toLex_mono.comp toDualProd_mono

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