feat: cardinality of the graph of a function (#18401)

From PFR

Author: YaelDillies

Mathlib/Data/Set/Card.lean

@@ -103,6 +103,8 @@ theorem encard_ne_zero : s.encard ≠ 0 ↔ s.Nonempty := by
 @[simp] theorem encard_pos : 0 < s.encard ↔ s.Nonempty := by
   rw [pos_iff_ne_zero, encard_ne_zero]
 
+protected alias ⟨_, Nonempty.encard_pos⟩ := encard_pos
+
 @[simp] theorem encard_singleton (e : α) : ({e} : Set α).encard = 1 := by
   rw [encard, ← PartENat.withTopEquiv.symm.injective.eq_iff, Equiv.symm_apply_apply,
     PartENat.card_eq_coe_fintype_card, Fintype.card_ofSubsingleton, Nat.cast_one]; rfl
@@ -530,6 +532,8 @@ theorem ncard_univ (α : Type*) : (univ : Set α).ncard = Nat.card α := by
 theorem ncard_pos (hs : s.Finite := by toFinite_tac) : 0 < s.ncard ↔ s.Nonempty := by
   rw [pos_iff_ne_zero, Ne, ncard_eq_zero hs, nonempty_iff_ne_empty]
 
+protected alias ⟨_, Nonempty.ncard_pos⟩ := ncard_pos
+
 theorem ncard_ne_zero_of_mem {a : α} (h : a ∈ s) (hs : s.Finite := by toFinite_tac) : s.ncard ≠ 0 :=
   ((ncard_pos hs).mpr ⟨a, h⟩).ne.symm
 
@@ -789,6 +793,9 @@ theorem inj_on_of_surj_on_of_ncard_le {t : Set β} (f : ∀ a ∈ s, β) (hf : 
       (by { rwa [← ncard_eq_toFinset_card', ← ncard_eq_toFinset_card'] }) a₁
       (by simpa) a₂ (by simpa) (by simpa)
 
+@[simp] lemma ncard_graphOn (s : Set α) (f : α → β) : (s.graphOn f).ncard = s.ncard := by
+  rw [← ncard_image_of_injOn fst_injOn_graph, image_fst_graphOn]
+
 section Lattice
 
 theorem ncard_union_add_ncard_inter (s t : Set α) (hs : s.Finite := by toFinite_tac)

Mathlib/SetTheory/Cardinal/Finite.lean

@@ -224,13 +224,22 @@ theorem card_zmod (n : ℕ) : Nat.card (ZMod n) = n := by
 end Nat
 
 namespace Set
+variable {s : Set α}
 
 lemma card_singleton_prod (a : α) (t : Set β) : Nat.card ({a} ×ˢ t) = Nat.card t := by
   rw [singleton_prod, Nat.card_image_of_injective (Prod.mk.inj_left a)]
 
 lemma card_prod_singleton (s : Set α) (b : β) : Nat.card (s ×ˢ {b}) = Nat.card s := by
   rw [prod_singleton, Nat.card_image_of_injective (Prod.mk.inj_right b)]
 
+theorem natCard_pos (hs : s.Finite) : 0 < Nat.card s ↔ s.Nonempty := by
+  simp [pos_iff_ne_zero, Nat.card_eq_zero, hs.to_subtype, Set.nonempty_def, nonempty_iff_ne_empty]
+
+protected alias ⟨_, Nonempty.natCard_pos⟩ := natCard_pos
+
+@[simp] lemma natCard_graphOn (s : Set α) (f : α → β) : Nat.card (s.graphOn f) = Nat.card s := by
+  rw [← Nat.card_image_of_injOn fst_injOn_graph, image_fst_graphOn]
+
 end Set
 
 namespace PartENat