not_strictMono_of_wellFoundedGT — Mathlib

English

In a preorder with WellFoundedGT, there is no StrictMono f: ℕ → α.

Русский

В предпорядке с хорошо основанным GT не существует строго монотонной функции f: ℕ → α.

LaTeX

$$$$\forall f:\mathbb{N} \to \alpha,\ \neg \mathrm{StrictMono}(f).$$$$

Lean4

theorem not_strictMono_of_wellFoundedGT [Preorder α] [WellFoundedGT α] (f : ℕ → α) : ¬StrictMono f :=
  not_strictAnti_of_wellFoundedLT (α := αᵒᵈ) f

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