strictMono_map_iff — Mathlib

English

For any f : ℕ → α with Preorder α, StrictMono (ENat.map f) iff StrictMono f.

Русский

Для любого f : ℕ → α с предпорядком α верно: StrictMono (ENat.map f) ⇔ StrictMono f.

LaTeX

$$$$\forall f : \mathbb{N} \to \alpha,\ [\text{Preorder } \alpha] \Rightarrow (\text{StrictMono}(\text{ENat.map } f) \iff \text{StrictMono}(f)).$$$$

Lean4

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

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