Documentation Verification Report

Girth

📁 Source: Mathlib/Combinatorics/SimpleGraph/Girth.lean

Statistics

Metric	Count
Definitions `egirth`, `girth`	2
Theorems `egirth_eq_top`, `girth_eq_zero`, `egirth_anti`, `egirth_bot`, `egirth_eq_top`, `egirth_le_length`, `exists_egirth_eq_length`, `exists_girth_eq_length`, `girth_anti`, `girth_bot`, `girth_eq_zero`, `girth_le_length`, `le_egirth`, `three_le_egirth`, `three_le_girth`	15
Total	17

SimpleGraph

Definitions

Name	Category	Theorems
`egirth` 📖	CompOp	8 math math: `exists_egirth_eq_length`, `three_le_egirth`, `egirth_eq_top`, `egirth_bot`, `egirth_le_length`, `egirth_anti`, `le_egirth`, `IsAcyclic.egirth_eq_top`
`girth` 📖	CompOp	7 math math: `exists_girth_eq_length`, `girth_eq_zero`, `girth_bot`, `girth_anti`, `girth_le_length`, `three_le_girth`, `IsAcyclic.girth_eq_zero`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`egirth_anti` 📖	mathematical	—	`Antitone` `SimpleGraph` `ENat` `PartialOrder.toPreorder` `instPartialOrder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `egirth`	—	`iInf_mono` `iInf₂_mono'` `Walk.IsCycle.mapLe` `Walk.length_map`
`egirth_bot` 📖	mathematical	—	`egirth` `Bot.bot` `SimpleGraph` `BooleanAlgebra.toBot` `CompleteBooleanAlgebra.toBooleanAlgebra` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `completeAtomicBooleanAlgebra` `Top.top` `ENat` `instTopENat`	—	—
`egirth_eq_top` 📖	mathematical	—	`egirth` `Top.top` `ENat` `instTopENat` `IsAcyclic`	—	—
`egirth_le_length` 📖	mathematical	`Walk.IsCycle`	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `egirth` `ENat.instNatCast` `Walk.length`	—	`le_egirth` `le_rfl`
`exists_egirth_eq_length` 📖	mathematical	—	`Walk.IsCycle` `egirth` `ENat` `ENat.instNatCast` `Walk.length` `IsAcyclic`	—	`iInf_subtype'` `iInf_sigma'` `ciInf_mem`
`exists_girth_eq_length` 📖	mathematical	—	`Walk.IsCycle` `girth` `Walk.length` `IsAcyclic`	—	`exists_egirth_eq_length`
`girth_anti` 📖	mathematical	`SimpleGraph` `instLE` `IsAcyclic`	`girth`	—	`ENat.toNat_le_toNat` `egirth_anti` `Iff.not` `egirth_eq_top`
`girth_bot` 📖	mathematical	—	`girth` `Bot.bot` `SimpleGraph` `BooleanAlgebra.toBot` `CompleteBooleanAlgebra.toBooleanAlgebra` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `completeAtomicBooleanAlgebra`	—	`egirth_bot`
`girth_eq_zero` 📖	mathematical	—	`girth` `IsAcyclic`	—	`Function.mt` `three_le_girth`
`girth_le_length` 📖	mathematical	`Walk.IsCycle`	`girth` `Walk.length`	—	`ENat.coe_le_coe` `LE.le.trans` `ENat.coe_toNat_le_self` `egirth_le_length`
`le_egirth` 📖	mathematical	—	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `egirth` `ENat.instNatCast` `Walk.length`	—	—
`three_le_egirth` 📖	mathematical	—	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `instOfNatAtLeastTwo` `ENat.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `egirth`	—	`Nat.instAtLeastTwoHAddOfNat` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsOrderedRing.toZeroLEOneClass` `Walk.IsCycle.three_le_length`
`three_le_girth` 📖	mathematical	`IsAcyclic`	`girth`	—	`ENat.toNat_le_toNat` `Nat.instAtLeastTwoHAddOfNat` `three_le_egirth` `Iff.not` `egirth_eq_top`

SimpleGraph.IsAcyclic

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`egirth_eq_top` 📖	mathematical	`SimpleGraph.IsAcyclic`	`SimpleGraph.egirth` `Top.top` `ENat` `instTopENat`	—	`SimpleGraph.egirth_eq_top`
`girth_eq_zero` 📖	mathematical	`SimpleGraph.IsAcyclic`	`SimpleGraph.girth`	—	`SimpleGraph.girth_eq_zero`

---

← Back to Index