FormalConjecturesForMathlib/Combinatorics/SimpleGraph/Cycle.lean

GitHub source file

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL
Lean4 Domain Explanation Language

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

5 declarations, 0 contain sorry, 0 declared as axioms

Imports (1)
Imported by 1 file
  1. structure SimpleGraph.Cycle A cycle of G, carrying its basepoint line 28 source

    Source documentation

    A cycle of G, carrying its basepoint. Bundling the basepoint makes the cycles of G into a type, so they can be collected into a Finset or a Multiset.

    no axioms what this means

    Statement uses: SimpleGraph

    structure Cycle (G : SimpleGraph V) where
…
  2. def SimpleGraph.Cycle.edges The edges a cycle traverses line 37 source

    Source documentation

    The edges a cycle traverses.

    no axioms what this means

    Statement uses: SimpleGraph, SimpleGraph.Cycle, List, Sym2

    Proof uses: SimpleGraph.Walk.edges, SimpleGraph.Cycle.base, SimpleGraph.Cycle.walk

    def Cycle.edges {G : SimpleGraph V} (c : Cycle G) : List (Sym2 V) := c.walk.edges

    Mentions: c, SimpleGraph.Cycle

  3. def SimpleGraph.Cycle.length The length of a cycle, its number of edges line 40 source

    Source documentation

    The length of a cycle, its number of edges.

    no axioms what this means

    Statement uses: SimpleGraph, SimpleGraph.Cycle, Nat

    Proof uses: SimpleGraph.Walk.length, SimpleGraph.Cycle.base, SimpleGraph.Cycle.walk

    def Cycle.length {G : SimpleGraph V} (c : Cycle G) : ℕ := c.walk.length

    Mentions: c, SimpleGraph.Cycle

  4. def SimpleGraph.IsBridgeless G is bridgeless if none of its edges is a bridge line 43 source

    Source documentation

    G is bridgeless if none of its edges is a bridge.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: SimpleGraph

    Proof uses: Sym2, Membership.mem, Set, SimpleGraph.edgeSet, Not, SimpleGraph.IsBridge

    1 instances, coercions and auxiliary constants left out.

    def IsBridgeless (G : SimpleGraph V) : Prop := ∀ e ∈ G.edgeSet, ¬ G.IsBridge e
  5. theorem SimpleGraph.edgeFinset_eq_empty_of_isBridgeless_of_isAcyclic In a forest every edge is a bridge, so an acyclic bridgeless graph has no edges at all line 46 source

    Source documentation

    In a forest every edge is a bridge, so an acyclic bridgeless graph has no edges at all.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Fintype, SimpleGraph, DecidableRel, SimpleGraph.Adj, SimpleGraph.IsAcyclic, SimpleGraph.IsBridgeless, Eq, Finset, Sym2, SimpleGraph.edgeFinset, EmptyCollection.emptyCollection

    Proof uses: Eq.mpr, Bot.bot, id, congrArg, propext, SimpleGraph.edgeFinset_eq_empty, SimpleGraph.ext, funext, Iff, Not, Eq.trans, False, iff_false, Sym2.mk, Iff.mp, Membership.mem, Set, SimpleGraph.edgeSet, SimpleGraph.IsBridge, SimpleGraph.isAcyclic_iff_forall_isBridge

    12 instances, coercions and auxiliary constants left out.

    Tactic trace: 5 steps

    Open to load the checked before-and-after goal states.

    theorem edgeFinset_eq_empty_of_isBridgeless_of_isAcyclic [Fintype V] (G : SimpleGraph V)
    [DecidableRel G.Adj] (hacyc : G.IsAcyclic) (hbr : G.IsBridgeless) : G.edgeFinset = ∅ := by
…