@@ -42,64 +42,6 @@ assert_not_exists Field
4242namespace SimpleGraph
4343variable {α : Type *} {G G' : SimpleGraph α}
4444
45- section eccent
46-
47- /-- The eccentricity of a vertex is the greatest distance between it and any other vertex. -/
48- noncomputable def eccent (G : SimpleGraph α) (u : α) : ℕ∞ :=
49- ⨆ v, G.edist u v
50-
51- lemma eccent_def : G.eccent = fun u ↦ ⨆ v, G.edist u v := rfl
52-
53- lemma edist_le_eccent {u v : α} : G.edist u v ≤ G.eccent u :=
54- le_iSup (G.edist u) v
55-
56- lemma exists_edist_eq_eccent_of_finite [Finite α] (u : α) :
57- ∃ v, G.edist u v = G.eccent u :=
58- have : Nonempty α := Nonempty.intro u
59- exists_eq_ciSup_of_finite
60-
61- lemma eccent_eq_top_of_not_connected (h : ¬ G.Connected) (u : α) :
62- G.eccent u = ⊤ := by
63- rw [connected_iff_exists_forall_reachable] at h
64- push_neg at h
65- obtain ⟨v, h⟩ := h u
66- rw [eq_top_iff, ← edist_eq_top_of_not_reachable h]
67- exact le_iSup (G.edist u) v
68-
69- lemma eccent_eq_zero_of_subsingleton [Subsingleton α] (u : α) : G.eccent u = 0 := by
70- simpa [eccent, edist_eq_zero_iff] using subsingleton_iff.mp ‹_› u
71-
72- lemma eccent_ne_zero [Nontrivial α] (u : α) : G.eccent u ≠ 0 := by
73- obtain ⟨v, huv⟩ := exists_ne ‹_›
74- contrapose! huv
75- simp only [eccent, ENat.iSup_eq_zero, edist_eq_zero_iff] at huv
76- exact (huv v).symm
77-
78- lemma eccent_eq_zero_iff (u : α) : G.eccent u = 0 ↔ Subsingleton α := by
79- refine ⟨fun h ↦ ?_, fun _ ↦ eccent_eq_zero_of_subsingleton u⟩
80- contrapose! h
81- rw [not_subsingleton_iff_nontrivial] at h
82- exact eccent_ne_zero u
83-
84- lemma eccent_pos_iff (u : α) : 0 < G.eccent u ↔ Nontrivial α := by
85- rw [pos_iff_ne_zero, ← not_subsingleton_iff_nontrivial, ← eccent_eq_zero_iff]
86-
87- @[simp]
88- lemma eccent_bot [Nontrivial α] (u : α) : (⊥ : SimpleGraph α).eccent u = ⊤ :=
89- eccent_eq_top_of_not_connected bot_not_connected u
90-
91- @[simp]
92- lemma eccent_top [Nontrivial α] (u : α) : (⊤ : SimpleGraph α).eccent u = 1 := by
93- apply le_antisymm ?_ <| Order.one_le_iff_pos.mpr <| pos_iff_ne_zero.mpr <| eccent_ne_zero u
94- rw [eccent, iSup_le_iff]
95- intro v
96- cases eq_or_ne u v <;> simp_all [edist_top_of_ne]
97-
98- proof_wanted eq_top_iff_forall_eccent_eq_one [Nontrivial α] :
99- G = ⊤ ↔ ∀ u, G.eccent u = 1
100-
101- end eccent
102-
10345/--
10446The diameter is the greatest distance between any two vertices. If the graph is disconnected,
10547this will be `0`.
@@ -114,34 +56,6 @@ lemma nontrivial_of_diam_ne_zero' (h : G.diam ≠ 0) : Nontrivial α := by
11456 rw [not_nontrivial_iff_subsingleton] at h
11557 exact diam_eq_zero_of_subsingleton
11658
117- section radius
118-
119- /-- The radius of a graph is the minimum eccentricity of its vertices. It's `⊤` for the empty
120- graph. -/
121- noncomputable def radius (G : SimpleGraph α) : ℕ∞ :=
122- ⨅ u, G.eccent u
123-
124- /-- The center of a graph is the set of vertices with minimum eccentricity. -/
125- noncomputable def center (G : SimpleGraph α) : Set α :=
126- {u | G.eccent u = G.radius}
127-
128- lemma center_def : G.center = {u | G.eccent u = G.radius} := rfl
129-
130- lemma radius_le_eccent {u : α} : G.radius ≤ G.eccent u :=
131- iInf_le G.eccent u
132-
133- proof_wanted radius_le_ediam : G.radius ≤ G.ediam
134-
135- lemma exists_eccent_eq_radius_of_finite [Nonempty α] [Finite α] :
136- ∃ u, G.eccent u = G.radius :=
137- exists_eq_ciInf_of_finite
138-
139- lemma center_nonempty_of_finite [Nonempty α] [Finite α] : G.center.Nonempty :=
140- exists_eccent_eq_radius_of_finite
141-
142- proof_wanted diam_le_two_mul_radius (h : G.center.Nonempty) : G.diam ≤ 2 * G.radius
143-
144- end radius
14559
14660section Path
14761open Path
0 commit comments