Theorems · Theorem · logic and foundations
Denumerable.ofNat_encode
∀ {α : Type u_1} [inst : Denumerable α] (a : α), Denumerable.ofNat α (Encodable.encode a) = a- Defined in
- Mathlib.Logic.Denumerable
- Cited by
- 8 results in Mathlib
- Foundations
- Depth 16 from the axioms · uses propext, Quot.sound
- Assumes
- Denumerable
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Encodable.encodestatement · cited by 118
- Denumerablestatement and proof · cited by 28
- Encodable.encodekproof · cited by 27
- Denumerable.ofNatstatement · cited by 26
- Denumerable.ofNat_of_decodeproof · cited by 4
Cited by9
Results whose statement or proof uses this declaration.
- Denumerable.eqvproof · cited by 6
- PeriodPair.summable_weierstrassPExceptSummandproof · cited by 3
- Nat.Partrec.Code.primrec_evalnproof · cited by 3
- Nat.Partrec'.of_partproof · cited by 2
- Nat.Partrec.Code.fixed_pointproof · cited by 1
- Nat.Partrec.Code.fixed_point₂proof · cited by 1
- Nat.Partrec.Code.primrec_recOn'proof · cited by 1
- Denumerable.list_ofNat_zeroproof · cited by 0
- Nat.Partrec.Code.computable_recOnproof · cited by 0