feat(Combinatorics/SimpleGraph/Bipartite): upper bound on the number of edges of a bipartite graph

Mathlib/Combinatorics/SimpleGraph/Basic.lean

@@ -559,6 +559,9 @@ theorem adj_iff_exists_edge {v w : V} : G.Adj v w ↔ v ≠ w ∧ ∃ e ∈ G.ed
 theorem adj_iff_exists_edge_coe : G.Adj a b ↔ ∃ e : G.edgeSet, e.val = s(a, b) := by
   simp only [mem_edgeSet, exists_prop, SetCoe.exists, exists_eq_right]
 
+theorem edgeSet_eq : G.edgeSet = { x | ∃ v w : V, x = s(v, w) ∧ G.Adj v w } :=
+  Set.ext <| Sym2.ind fun v w ↦ ⟨fun h ↦ ⟨v, w, rfl, h⟩, by grind [mem_edgeSet]⟩
+
 variable (G G₁ G₂)
 
 theorem edge_other_ne {e : Sym2 V} (he : e ∈ G.edgeSet) {v : V} (h : v ∈ e) :

Mathlib/Combinatorics/SimpleGraph/Bipartite.lean

@@ -445,4 +445,59 @@ theorem degree_le_between_add_compl (hw : w ∈ sᶜ) :
 
 end Between
 
+section
+
+variable {W₁ W₂ : Type*}
+
+theorem completeBipartiteGraph_edgeSet : (completeBipartiteGraph W₁ W₂).edgeSet =
+    Set.range (fun x : W₁ × W₂ ↦ s(.inl x.1, .inr x.2)) := by
+  refine Set.ext <| Sym2.ind fun u v ↦ ⟨fun h ↦ ?_, fun ⟨⟨a, b⟩, z⟩ ↦ ?_⟩
+  · cases u <;> cases v <;> simp_all
+  · grind [completeBipartiteGraph_adj, mem_edgeSet]
+
+theorem completeBipartiteGraph_edgeSet_encard :
+    (completeBipartiteGraph W₁ W₂).edgeSet.encard = ENat.card W₁ * ENat.card W₂ := by
+  rw [completeBipartiteGraph_edgeSet, ← ENat.card_prod, ← Set.encard_univ, ← Set.image_univ]
+  exact Function.Injective.encard_image (by grind [Function.Injective]) Set.univ
+
+theorem IsBipartiteWith.nonempty_embedding_completeBipartiteGraph_edgeSet
+    (hG : G.IsBipartiteWith s t) :
+    Nonempty (G.edgeSet ↪ (completeBipartiteGraph s t).edgeSet) := by
+  refine ⟨⟨fun ⟨x, hx⟩ ↦ ?_, fun _ _ _ ↦ ?_⟩⟩
+  · by_cases! h : x.out.1 ∈ s
+    · refine ⟨s(.inl ⟨x.out.1, h⟩, .inr ⟨x.out.2, ?_⟩), by simp⟩
+      grind [hG.disjoint, hG.mem_of_adj, edgeSet_eq, Sym2.eq_out]
+    · refine ⟨s(.inr ⟨x.out.1, ?_⟩, .inl ⟨x.out.2, ?_⟩), by simp⟩
+      · grind [hG.mem_of_adj <| G.mem_edgeSet.mpr <| Sym2.eq_out x ▸ hx]
+      · grind [hG.disjoint, hG.mem_of_adj, edgeSet_eq, Sym2.eq_out]
+  · grind [Sym2.eq_out]
+
+end
+
+section
+
+/-- An upper bound on the cardinality of the edge set of a bipartite graph when the vertex sets
+forming it may also be infinite: in that case as well, the upper bound is the product of
+the cardinalities of these two sets. The statement uses `Set.encard`. -/
+theorem IsBipartiteWith.encard_edgeSet_le (hG : G.IsBipartiteWith s t) :
+    G.edgeSet.encard ≤ s.encard * t.encard := by
+  grw [hG.nonempty_embedding_completeBipartiteGraph_edgeSet.some.encard_le]
+  simp [completeBipartiteGraph_edgeSet_encard]
+
+/-- An upper bound on the cardinality of the edge set of a bipartite graph when the cardinality
+of the entire vertex set of the graph is known. That is, the cardinality of the edge set times `4`
+is less or equal to the square of the cardinality of the vertex set.
+The statement uses `Set.encard` and `ENat.card`. -/
+theorem IsBipartite.four_mul_encard_edgeSet_le (h : G.IsBipartite) :
+    4 * G.edgeSet.encard ≤ ENat.card V ^ 2 := by
+  refine finite_or_infinite V |>.elim (fun hv ↦ ?_) (fun _ ↦ by simp)
+  have ⟨s, t, h⟩ := h.exists_isBipartiteWith
+  grw [h.encard_edgeSet_le]
+  have := Set.encard_union_eq h.disjoint ▸ Set.encard_le_card
+  rw [ENat.card_eq_coe_natCard, ← s.toFinite.cast_ncard_eq, ← t.toFinite.cast_ncard_eq] at this ⊢
+  norm_cast at this ⊢
+  grind [Nat.pow_le_pow_left this 2, four_mul_le_sq_add s.ncard t.ncard]
+
+end
+
 end SimpleGraph

Mathlib/Data/Sym/Sym2.lean

@@ -353,6 +353,8 @@ theorem out_fst_mem (e : Sym2 α) : e.out.1 ∈ e :=
 theorem out_snd_mem (e : Sym2 α) : e.out.2 ∈ e :=
   ⟨e.out.1, by rw [eq_swap, Sym2.mk, e.out_eq]⟩
 
+theorem eq_out (e : Sym2 α) : e = s(e.out.1, e.out.2) := Sym2.ext (by simp)
+
 theorem ball {p : α → Prop} {a b : α} : (∀ c ∈ s(a, b), p c) ↔ p a ∧ p b := by
   simp