Mathlib Map

Theorems · Theorem · logic and foundations

ENat.card_eq_top_of_infinite

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

Around this declaration

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

Set.Infinite.encard_eq · cited by 6Infinite.encard_eqModule.length_finsupp · cited by 2Module.length_finsuppENNReal.toReal_enatCard · cited by 1ENNReal.toReal_enatCardIsOpenMap.enatCard_connectedComponents_le_encard_preimage_singleton · cited by 1IsOpenMap.enatCard_connec…List.Nodup.length_le_enatCard · cited by 1Nodup.length_le_enatCardSubmodule.exists_forall_notMem_of_forall_ne_top · cited by 1Submodule.exists_forall_n…SimpleGraph.chromaticNumber_top_eq_enat_card · cited by 0SimpleGraph.chromaticNumb…ringKrullDim_add_enatCard_le_ringKrullDim_mvPolynomial · cited by 0ringKrullDim_add_enatCard…SimpleGraph.IsBipartite.four_mul_encard_edgeSet_le · cited by 0IsBipartite.four_mul_enca…ENat.card_fun · cited by 0ENat.card_funModule.length_pi · cited by 0Module.length_piTop.top · cited by 9680Top.topENat · cited by 4985ENatInfinite · cited by 352InfiniteENat.card · cited by 89ENat.cardENat.card_eq_top_of_infiniteCITED 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 by11

Results whose statement or proof uses this declaration.