Theorems · Definition · combinatorics
SimpleGraph.LocallyFinite
{V : Type u_1} → SimpleGraph V → Type u_1A graph is locally finite if every vertex has a finite neighbor set.
- Defined in
- Mathlib.Combinatorics.SimpleGraph.Finite
- Cited by
- 18 results in Mathlib
- Foundations
- Depth 5 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Fintypeproof · cited by 7,736
- Set.Elemproof · cited by 7,166
- SimpleGraphstatement and proof · cited by 3,072
- SimpleGraph.neighborSetproof · cited by 257
Cited by21
Results whose statement or proof uses this declaration.
- SimpleGraph.IsRegularOfDegreestatement and proof · cited by 10
- SimpleGraph.finsetWalkLengthstatement and proof · cited by 8
- SimpleGraph.IsRegularOfDegree.degree_eqstatement and proof · cited by 3
- SimpleGraph.coe_finsetWalkLength_eqstatement and proof · cited by 2
- SimpleGraph.finsetWalkLengthLTstatement and proof · cited by 2
- SimpleGraph.union_eq_univ_of_forall_ncard_lestatement and proof · cited by 2
- SimpleGraph.coe_finsetWalkLengthLT_eqstatement and proof · cited by 1
- SimpleGraph.exists_bijective_of_forall_ncard_lestatement and proof · cited by 1
- SimpleGraph.isBipartiteWith_sum_degrees_eqstatement and proof · cited by 1
- SimpleGraph.card_set_walk_length_eqstatement and proof · cited by 1
- SimpleGraph.nonempty_ends_of_infinitestatement and proof · cited by 0
- SimpleGraph.set_walk_length_toFinset_eqstatement and proof · cited by 0