Mathlib Map

Theorems · Definition · order theory

ENat.recTopCoe

{C : ℕ∞ → Sort u_1} → C ⊤ → ((a : ℕ) → C ↑a) → (n : ℕ∞) → C n

Recursor for ENat using the preferred forms ⊤ and ↑a.

Defined in
Mathlib.Data.ENat.Defs
Cited by
75 results in Mathlib
Foundations
Depth 5 from the axioms · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

FiniteMultiplicity.emultiplicity_eq_multiplicity · cited by 31FiniteMultiplicity.emulti…Ring.ordMonoidWithZeroHom · cited by 12Ring.ordMonoidWithZeroHomENat.natCast_toNat_eq_self · cited by 9ENat.natCast_toNat_eq_selfAnalyticAt.meromorphicOrderAt_eq · cited by 9AnalyticAt.meromorphicOrd…PowerSeries.le_order · cited by 7PowerSeries.le_orderENat.one_epow · cited by 7ENat.one_epowMvPowerSeries.le_weightedOrder · cited by 7MvPowerSeries.le_weighted…ENat.natCast_toNat_le_self · cited by 6ENat.natCast_toNat_le_selfIsDiscreteValuationRing.idealOrderIsoENat · cited by 5IsDiscreteValuationRing.i…Order.height_le_coe_iff · cited by 5Order.height_le_coe_iffENat.ceil_le · cited by 4ENat.ceil_leENat.toNat_eq_iff · cited by 4ENat.toNat_eq_iffENat.toNat_mul · cited by 4ENat.toNat_mulOrder.exists_series_of_le_height · cited by 4Order.exists_series_of_le…ENat.zero_epow · cited by 4ENat.zero_epowTop.top · cited by 9680Top.topENat · cited by 4985ENatENat.recTopCoeCITED BYCITES

Cites2

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

  • Top.topstatement and proof · cited by 9,680
  • ENatstatement and proof · cited by 4,985

Cited by77

Results whose statement or proof uses this declaration.