ENat.card

Type u_3 → ℕ∞

ENat.card α is the cardinality of α as an extended natural number. If α is infinite, ENat.card α = ⊤.

Defined in: Mathlib.SetTheory.Cardinal.Finite
Cited by: 89 results in Mathlib
Foundations: Depth 88 from the axioms · uses propext, Classical.choice, Quot.sound

Around this declaration

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

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

Results whose statement or proof uses this declaration.

Set.encardproof · cited by 327
ENat.card_eq_coe_fintype_cardstatement · cited by 15
Set.encard_univstatement and proof · cited by 15
Set.InjOn.encard_imageproof · cited by 13
ENat.card_eq_coe_natCardstatement · cited by 12
ENat.card_eq_top_of_infinitestatement · cited by 11
ENat.card_congrstatement · cited by 8
MeasureTheory.Measure.count_univstatement and proof · cited by 4
ENat.card_lt_topstatement · cited by 4
Fin.Embedding.restrictSurjective_of_add_le_ENatCardstatement and proof · cited by 4
SimpleGraph.vertexCoverNum_le_card_sub_onestatement and proof · cited by 3
ENat.card_eq_topstatement · cited by 3