Theorems · Theorem · number theory

Nat.nth_le_of_strictMonoOn_of_mapsTo

∀ {p : ℕ → Prop} (f : ℕ → ℕ),
  Set.MapsTo f {n | ∀ (hf : (Set.ofPred p).Finite), n < hf.toFinset.card} (Set.ofPred p) →
    StrictMonoOn f {n | ∀ (hf : (Set.ofPred p).Finite), n < hf.toFinset.card} → ∀ {n : ℕ}, Nat.nth p n ≤ f n

Nat.nth p is the least strictly monotone function whose image is contained in Set.ofPred p

Defined in

Mathlib.Data.Nat.Nth

Cited by

1 results in Mathlib

Foundations

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