From 5024c93693c201b2cb4bb166bfea17cbda5e706e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Mon, 30 Sep 2024 17:40:35 +0000 Subject: [PATCH] =?UTF-8?q?feat:=20`Disjoint=20G=E2=82=81.edgeFinset=20G?= =?UTF-8?q?=E2=82=82.edgeFinset=20=E2=86=94=20Disjoint=20G=E2=82=81=20G?= =?UTF-8?q?=E2=82=82`=20(#17286)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit From LeanCamCombi --- Mathlib/Combinatorics/SimpleGraph/Finite.lean | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/Mathlib/Combinatorics/SimpleGraph/Finite.lean b/Mathlib/Combinatorics/SimpleGraph/Finite.lean index 278ba02e0df80..bab7f40b821df 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Finite.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Finite.lean @@ -92,6 +92,15 @@ theorem edgeFinset_inf [DecidableEq V] : (G₁ ⊓ G₂).edgeFinset = G₁.edgeF theorem edgeFinset_sdiff [DecidableEq V] : (G₁ \ G₂).edgeFinset = G₁.edgeFinset \ G₂.edgeFinset := by simp [edgeFinset] +lemma disjoint_edgeFinset : Disjoint G₁.edgeFinset G₂.edgeFinset ↔ Disjoint G₁ G₂ := by + simp_rw [← Finset.disjoint_coe, coe_edgeFinset, disjoint_edgeSet] + +lemma edgeFinset_eq_empty : G.edgeFinset = ∅ ↔ G = ⊥ := by + rw [← edgeFinset_bot, edgeFinset_inj] + +lemma edgeFinset_nonempty : G.edgeFinset.Nonempty ↔ G ≠ ⊥ := by + rw [Finset.nonempty_iff_ne_empty, edgeFinset_eq_empty.ne] + theorem edgeFinset_card : G.edgeFinset.card = Fintype.card G.edgeSet := Set.toFinset_card _