Theorems · Definition · number theory

Nat.giCountNth

{p : ℕ → Prop} → [inst : DecidablePred p] → (Set.ofPred p).Infinite → GaloisInsertion (Nat.count p) (Nat.nth p)

If a predicate p : ℕ → Prop is true for infinitely many numbers, then Nat.count p and Nat.nth p form a Galois insertion.

Defined in

Mathlib.Data.Nat.Nth

Cited by

1 results in Mathlib

Foundations

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

Assumes

DecidablePred