Mathlib Map

Theorems · Theorem · order theory

ENat.natCast_ne_top

∀ (a : ℕ), ↑a ≠ ⊤
Defined in
Mathlib.Data.ENat.Basic
Cited by
21 results in Mathlib
Foundations
Depth 11 from the axioms · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Dynamics.coverMincard_finite_iff · cited by 6Dynamics.coverMincard_fin…ENat.toNat_le_of_le_natCast · cited by 5ENat.toNat_le_of_le_natCa…ENat.lt_natCast_add_one_iff · cited by 4ENat.lt_natCast_add_one_i…AnalyticAt.analyticOrderAt_deriv_add_one · cited by 2AnalyticAt.analyticOrderA…Set.powersetCard.exists_mem_notMem · cited by 2powersetCard.exists_mem_n…ModularForm.sturm_bound_levelOne_nat · cited by 1ModularForm.sturm_bound_l…ENat.WithBot.add_one_le_iff · cited by 1WithBot.add_one_le_iffENat.WithBot.lt_add_one_iff · cited by 1WithBot.lt_add_one_iffAddMonoid.minOrder_eq_top · cited by 1AddMonoid.minOrder_eq_topENat.add_one_le_natCast_iff · cited by 1ENat.add_one_le_natCast_i…ENat.natCast_add_one_le_iff · cited by 1ENat.natCast_add_one_le_i…ENat.natCast_lt_add_one_iff · cited by 1ENat.natCast_lt_add_one_i…SimpleGraph.exists_walk_of_edist_eq_coe · cited by 1SimpleGraph.exists_walk_o…UniqueFactorizationMonoid.pow_dvd_pow_iff_dvd · cited by 0UniqueFactorizationMonoid…CategoryTheory.projectiveDimension_ne_top_iff · cited by 0CategoryTheory.projective…Top.top · cited by 9680Top.topENat · cited by 4985ENatENat.natCast_ne_topCITED 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 · cited by 4,985

Cited by21

Results whose statement or proof uses this declaration.