Commit 2026-11-10 14:11 9e96668b

View on Github →

feat(Data/Set/Card): ncard of image2, and sets of a given ncard (#45617)

  • Set.ncard_image2_le : (image2 f s t).ncard ≤ s.ncard * t.ncard for finite s and t.
  • Set.Infinite.exists_superset_ncard_eq now also says that the superset is finite; new Set.exists_subset_ncard_eq, and Set.exists_superset_ncard_eq and Set.exists_ncard_eq in an infinite type.
  • Set.ncard_eq_zero_iff : s.ncard = 0 ↔ s = ∅ ∨ s.Infinite, as a simp lemma.
  • Data/Set/Card.lean gets set_option linter.style.longFile 1700.

Estimated changes

added theorem Set.exists_ncard_eq
added theorem Set.ncard_eq_zero_iff
added theorem Set.ncard_image2_le