Theorems · Theorem · combinatorics

SimpleGraph.card_filter_edgeFinset_toFinset_subset

∀ {V : Type u_1} [inst : Fintype V] {G : SimpleGraph V} [inst_1 : DecidableRel G.Adj] [inst_2 : DecidableEq V]
  (s : Finset V), {e ∈ G.edgeFinset | e.toFinset ⊆ s}.card = (SimpleGraph.induce (↑s) G).edgeFinset.card

The edges whose vertices lie in s are in bijection with the edges of the induced subgraph G.induce s.

Defined in

Mathlib.Combinatorics.SimpleGraph.Finite

Cited by

0 results in Mathlib

Foundations

Depth 78 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FintypeDecidableRelDecidableEq