def SimpleGraph.degOn {α : Type u_1} [Fintype α] [DecidableEq α] (G : SimpleGraph α) [DecidableRel G.Adj] (s : Finset α) (a : α) : ℕ

Number of vertices of s adjacent to a.

Equations

• G.degOn s a = (s ∩ G.neighborFinset a).card

theorem SimpleGraph.degOn_mono {α : Type u_1} [Fintype α] [DecidableEq α] (G : SimpleGraph α) [DecidableRel G.Adj] {s t : Finset α} (hst : s ⊆ t) (a : α) : G.degOn s a ≤ G.degOn t a

@[simp]

theorem SimpleGraph.degOn_empty {α : Type u_1} [Fintype α] [DecidableEq α] (G : SimpleGraph α) [DecidableRel G.Adj] (a : α) : G.degOn ∅ a = 0

@[simp]

theorem SimpleGraph.degOn_univ {α : Type u_1} [Fintype α] [DecidableEq α] (G : SimpleGraph α) [DecidableRel G.Adj] (a : α) : G.degOn Finset.univ a = G.degree a

theorem SimpleGraph.degOn_union {α : Type u_1} [Fintype α] [DecidableEq α] (G : SimpleGraph α) [DecidableRel G.Adj] {s t : Finset α} (h : Disjoint s t) (a : α) : G.degOn (s ∪ t) a = G.degOn s a + G.degOn t a

theorem SimpleGraph.sum_degOn_comm {α : Type u_1} [Fintype α] [DecidableEq α] (G : SimpleGraph α) [DecidableRel G.Adj] (s t : Finset α) : ∑ a ∈ s, G.degOn t a = ∑ a ∈ t, G.degOn s a