OAI/NumberTheory/TwoPoint/Walks/ForestLeaves.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Every finite nonempty forest has a vertex with at most one neighbor.

  1. theorem OAI.TwoPointCorrelations.finite_forest_has_leaf line 12

    Source documentation

    A degree-free formulation convenient for deleting a leaf in an induction.

    theorem finite_forest_has_leaf {V : Type*} [Fintype V] [Nonempty V]
    (G : SimpleGraph V) (hG : G.IsAcyclic) :
    ∃ x : V, ∀ y z : V, G.Adj x y → G.Adj x z → y = z := by
…