Mathlib Set.ncard vs Set.encard: ncard of an infinite set is 0
Checked on Mathlib v4.35.0. Set.ncard s = ENat.toNat s.encard (Set.ncard_def, rfl), so Set.Infinite.ncard : s.Infinite → s.ncard = 0. Hence ncard lemmas carry finiteness autoParams: Set.ncard_le_ncard (hst : s ⊆ t) (ht : t.Finite := by toFinite_tac) closes silently on Set (Fin 5), but on Set ℕ it fails with "could not synthesize default value for parameter 'ht' ... failed to synthesize Finite ↑t". The statement really is false there: {0} ⊆ univ, yet ncard univ = 0. Set.encard (in ℕ∞) needs no finiteness: Set.encard_le_encard h and Set.encard_union_eq (h : Disjoint s t) hold for all sets. Conversions: Set.ncard_coe_finset s : (↑s).ncard = s.card, Set.encard_coe_eq_coe_finsetCard s : (↑s).encard = ↑s.card, Set.Finite.cast_ncard_eq : s.Finite → ↑s.ncard = s.encard. Rule: state infinite-capable results with encard, and use ncard only when you can supply .Finite (or the ambient type is Finite).
Every claim checked on Mathlib v4.35.0.
s.ncard = ENat.toNat s.encardholds by rfl.Set.Infinite.ncard Set.infinite_univ : (univ : Set ℕ).ncard = 0typechecks.Set.ncard_le_ncard hcloses on Set (Fin 5) and on Set ℕ fails with 'could not synthesize default value for parameter 'ht''. The shapes of encard_le_encard, encard_union_eq (Disjoint s t), ncard_coe_finset, encard_coe_eq_coe_finsetCard and Finite.cast_ncard_eq are exactly as given.