monotone_map_iff — Mathlib

English

Let f: ℕ → α be a function into a preorder. Then ENat.map f is monotone if and only if f is monotone.

Русский

Пусть f: ℕ → α — функция в частично упорядоченном множестве. Тогда ENat.map f монотонно тогда и только тогда, когда f монотонна.

LaTeX

$$$$ \\operatorname{Monotone}(\\mathrm{ENat.map} \\; f) \\iff \\operatorname{Monotone} f $$$$

Lean4

@[simp]
theorem monotone_map_iff {f : ℕ → α} [Preorder α] : Monotone (ENat.map f) ↔ Monotone f :=
  WithTop.monotone_map_iff

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