Mathlib Map

Theorems · Theorem · logic and foundations

ENat.card_eq_top

∀ {α : Type u_1}, ENat.card α = ⊤ ↔ Infinite α
Defined in
Mathlib.SetTheory.Cardinal.Finite
Cited by
3 results in Mathlib
Foundations
Depth 91 from the axioms · uses propext, Classical.choice, Quot.sound
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

ENat.card_fun · cited by 0ENat.card_funMatrix.eRank_le_card_width · cited by 0Matrix.eRank_le_card_widthMatrix.eRank_le_card_height · cited by 0Matrix.eRank_le_card_heig…Top.top · cited by 9680Top.topENat · cited by 4985ENatInfinite · cited by 352InfiniteENat.card · cited by 89ENat.cardENat.card_eq_topCITED BYCITES

Cites4

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

  • Top.topstatement · cited by 9,680
  • ENatstatement · cited by 4,985
  • Infinitestatement and proof · cited by 352
  • ENat.cardstatement · cited by 89

Cited by3

Results whose statement or proof uses this declaration.