Theorems · Theorem · number theory

Nat.nth_comp_of_strictMono

∀ {p : ℕ → Prop} {n : ℕ} {f : ℕ → ℕ},
  StrictMono f →
    (∀ (k : ℕ), p k → k ∈ Set.range f) →
      (∀ (hfi : (Set.ofPred p).Finite), n < hfi.toFinset.card) → f (Nat.nth (fun i => p (f i)) n) = Nat.nth p n

Defined in: Mathlib.Data.Nat.Nth
Cited by: 1 results in Mathlib
Foundations: Depth 92 from the axioms · uses propext, Classical.choice, Quot.sound

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites22

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Setstatement and proof · cited by 53,352
Set.ofPredstatement and proof · cited by 6,101
Set.imageproof · cited by 5,609
Set.rangestatement and proof · cited by 4,705
Finset.cardstatement and proof · cited by 2,327
Set.extproof · cited by 2,266
Set.Finitestatement and proof · cited by 1,814
InfSet.sInfproof · cited by 935
StrictMonostatement and proof · cited by 706
LT.lt.transproof · cited by 370
Set.Finite.toFinsetstatement and proof · cited by 351
InfSetproof · cited by 145

Cited by1

Results whose statement or proof uses this declaration.

Nat.nth_addproof · cited by 2