Theorems · Theorem · order theory

Set.PartiallyWellOrderedOn.exists_monotone_subseq

∀ {α : Type u_2} {r : α → α → Prop} {s : Set α} [IsPreorder α r],
  s.PartiallyWellOrderedOn r → ∀ {f : ℕ → α}, (∀ (n : ℕ), f n ∈ s) → ∃ g, ∀ (m n : ℕ), m ≤ n → r (f (g m)) (f (g n))

Defined in

Mathlib.Order.WellFoundedSet

Cited by

9 results in Mathlib

Foundations

Depth 86 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

IsPreorder