Mathlib Map

Theorems · Definition · order theory

ENat

Type

Extended natural numbers ℕ∞ = WithTop ℕ.

Defined in
Mathlib.Data.ENat.Defs
Cited by
4,985 results in Mathlib
Foundations
Depth 2 from the axioms, rests on 4 definitions · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

ContDiff · cited by 352ContDiffSet.encard · cited by 327Set.encardIsManifold · cited by 326IsManifoldContDiffOn · cited by 294ContDiffOnContDiffWithinAt · cited by 283ContDiffWithinAtContMDiff · cited by 278ContMDiffContDiffAt · cited by 262ContDiffAtContMDiffOn · cited by 203ContMDiffOnContMDiffAt · cited by 192ContMDiffAtContMDiffWithinAt · cited by 189ContMDiffWithinAtemultiplicity · cited by 156emultiplicityENat.toNat · cited by 143ENat.toNatContMDiffMap · cited by 125ContMDiffMapContDiffMapSupportedIn · cited by 107ContDiffMapSupportedInContMDiffVectorBundle · cited by 106ContMDiffVectorBundleWithTop · cited by 3754WithTopENatCITED BYCITES

Cites1

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

Cited by5,472

Results whose statement or proof uses this declaration.

Showing the 200 most cited of 5,472.