not_strictAnti_of_wellFoundedLT — Mathlib

English

In a preorder with WellFoundedLT, any function f:_N → α cannot be StrictAnti.

Русский

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

LaTeX

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

Lean4

theorem not_strictAnti_of_wellFoundedLT [Preorder α] [WellFoundedLT α] (f : ℕ → α) : ¬StrictAnti f := fun hf ↦
  (RelEmbedding.natGT f (fun n ↦ hf (by simp))).not_wellFounded wellFounded_lt

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