not_wellFounded — Mathlib

English

If there exists an order-embedding of (ℕ, >) into r, then r is not well-founded.

Русский

Если существует вложение порядка от (ℕ, >) в r, то r не является хорошо основанным.

LaTeX

$$$$\forall f:\ ((\cdot > \cdot) : \mathbb{N} \to \mathbb{N} \to \mathrm{Prop}) \hookrightarrow_r r,\ \neg \mathrm{WellFounded}(r).$$$$

Lean4

theorem not_wellFounded (f : ((· > ·) : ℕ → ℕ → Prop) ↪r r) : ¬WellFounded r :=
  by
  rw [wellFounded_iff_isEmpty, not_isEmpty_iff]
  exact ⟨f⟩

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