Documentation Verification Report

Hamiltonian

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

Statistics

Metric	Count
Definitions `IsHamiltonian`, `IsHamiltonian`, `fintype`, `getVertEquiv`, `supportGetEquiv`, `IsHamiltonianCycle`	6
Theorems `connected`, `mono`, `of_card_eq_one`, `of_unique`, `getVertEquiv_apply`, `getVertEquiv_symm_apply`, `getVert_surjective`, `isPath`, `length_eq`, `length_support`, `map`, `mem_support`, `of_subsingleton`, `supportGetEquiv_apply`, `supportGetEquiv_symm_apply_val`, `support_toFinset`, `count_support_self`, `isCycle`, `isHamiltonian_tail`, `length_eq`, `map`, `mem_support`, `support_count_of_ne`, `toIsCycle`, `isHamiltonian_iff`, `isHamiltonian_of_mem`, `isHamiltonianCycle_iff_isCycle_and_length_eq`, `isHamiltonianCycle_iff_isCycle_and_support_count_tail_eq_one`, `isHamiltonianCycle_isCycle_and_isHamiltonian_tail`, `isHamiltonian_iff_isPath_and_length_eq`, `isHamiltonian_iff_support_get_bijective`, `not_isHamiltonian_bot_of_card_ne_one`, `not_isHamiltonian_of_card_eq_two`, `not_isHamiltonian_of_isBridge`, `not_isHamiltonian_of_isEmpty`	35
Total	41

SimpleGraph

Definitions

Name	Category	Theorems
`IsHamiltonian` 📖	MathDef	6 math math: `not_isHamiltonian_of_isEmpty`, `not_isHamiltonian_of_isBridge`, `IsHamiltonian.of_unique`, `not_isHamiltonian_bot_of_card_ne_one`, `IsHamiltonian.of_card_eq_one`, `not_isHamiltonian_of_card_eq_two`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`not_isHamiltonian_bot_of_card_ne_one` 📖	mathematical	—	`IsHamiltonian` `Bot.bot` `SimpleGraph` `BooleanAlgebra.toBot` `CompleteBooleanAlgebra.toBooleanAlgebra` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `completeAtomicBooleanAlgebra`	—	`Walk.adj_snd` `Walk.IsCycle.not_nil` `Walk.IsHamiltonianCycle.toIsCycle`
`not_isHamiltonian_of_card_eq_two` 📖	mathematical	`Fintype.card`	`IsHamiltonian`	—	—
`not_isHamiltonian_of_isBridge` 📖	mathematical	`Fintype.card` `IsBridge`	`IsHamiltonian`	—	`Sym2.ind` `Adj.ne` `isBridge_iff_adj_and_forall_walk_mem_edges` `ne_of_gt` `isBridge_iff_adj_and_forall_cycle_notMem` `Walk.IsHamiltonianCycle.isCycle` `Walk.IsHamiltonianCycle.mem_support` `Walk.IsCycle.rotate` `List.IsRotated.mem_iff` `Walk.rotate_edges` `Walk.start_mem_support` `Walk.IsHamiltonian.mem_support` `Walk.IsHamiltonianCycle.isHamiltonian_tail` `Walk.IsCycle.not_nil` `Walk.support_tail_of_not_nil` `List.IsRotated.perm` `Walk.support_rotate` `Walk.edges_takeUntil_subset`
`not_isHamiltonian_of_isEmpty` 📖	mathematical	—	`IsHamiltonian`	—	`IsEmpty.exists_iff` `Fintype.card_eq_zero`

SimpleGraph.IsHamiltonian

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`connected` 📖	mathematical	`SimpleGraph.IsHamiltonian`	`SimpleGraph.Connected`	—	`eq_or_ne` `SimpleGraph.Reachable.refl` `LT.lt.ne'` `Fintype.one_lt_card` `SimpleGraph.Walk.IsHamiltonianCycle.mem_support` `SimpleGraph.Walk.reachable` `not_isEmpty_iff` `SimpleGraph.not_isHamiltonian_of_isEmpty`
`mono` 📖	—	`SimpleGraph` `SimpleGraph.instLE` `SimpleGraph.IsHamiltonian`	—	—	`SimpleGraph.Walk.IsHamiltonianCycle.map` `Function.bijective_id`
`of_card_eq_one` 📖	mathematical	`Fintype.card`	`SimpleGraph.IsHamiltonian`	—	—
`of_unique` 📖	mathematical	—	`SimpleGraph.IsHamiltonian`	—	`of_card_eq_one` `Fintype.card_unique`

SimpleGraph.Walk

Definitions

Name	Category	Theorems
`IsHamiltonian` 📖	MathDef	7 math math: `IsPath.isHamiltonian_of_mem`, `IsHamiltonianCycle.isHamiltonian_tail`, `isHamiltonianCycle_isCycle_and_isHamiltonian_tail`, `isHamiltonian_iff_support_get_bijective`, `isHamiltonian_iff_isPath_and_length_eq`, `IsPath.isHamiltonian_iff`, `IsHamiltonian.of_subsingleton`
`IsHamiltonianCycle` 📖	CompData	3 math math: `isHamiltonianCycle_isCycle_and_isHamiltonian_tail`, `isHamiltonianCycle_iff_isCycle_and_length_eq`, `isHamiltonianCycle_iff_isCycle_and_support_count_tail_eq_one`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isHamiltonianCycle_iff_isCycle_and_length_eq` 📖	mathematical	—	`IsHamiltonianCycle` `IsCycle` `length` `Fintype.card`	—	`IsHamiltonianCycle.isCycle` `IsHamiltonianCycle.length_eq` `isHamiltonian_iff_isPath_and_length_eq` `IsCycle.isPath_tail`
`isHamiltonianCycle_iff_isCycle_and_support_count_tail_eq_one` 📖	mathematical	—	`IsHamiltonianCycle` `IsCycle` `support`	—	`support_tail_of_not_nil`
`isHamiltonianCycle_isCycle_and_isHamiltonian_tail` 📖	mathematical	—	`IsHamiltonianCycle` `IsCycle` `IsHamiltonian` `snd` `tail`	—	—
`isHamiltonian_iff_isPath_and_length_eq` 📖	mathematical	—	`IsHamiltonian` `IsPath` `length` `Fintype.card`	—	`IsHamiltonian.isPath` `IsHamiltonian.length_eq` `isPath_iff_injective_get_support` `isHamiltonian_iff_support_get_bijective` `Function.Injective.surjective_of_finite` `Finite.of_fintype` `length_support` `Fintype.card_ne_zero`
`isHamiltonian_iff_support_get_bijective` 📖	mathematical	—	`IsHamiltonian` `Function.Bijective` `support`	—	`List.get_bijective_iff`

SimpleGraph.Walk.IsHamiltonian

Definitions

Name	Category	Theorems
`fintype` 📖	CompOp	—
`getVertEquiv` 📖	CompOp	2 math math: `getVertEquiv_apply`, `getVertEquiv_symm_apply`
`supportGetEquiv` 📖	CompOp	3 math math: `getVertEquiv_symm_apply`, `supportGetEquiv_apply`, `supportGetEquiv_symm_apply_val`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`getVertEquiv_apply` 📖	mathematical	`SimpleGraph.Walk.IsHamiltonian`	`DFunLike.coe` `Equiv` `SimpleGraph.Walk.support` `EquivLike.toFunLike` `Equiv.instEquivLike` `getVertEquiv` `SimpleGraph.Walk.getVert`	—	—
`getVertEquiv_symm_apply` 📖	mathematical	`SimpleGraph.Walk.IsHamiltonian`	`DFunLike.coe` `Equiv` `SimpleGraph.Walk.support` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `getVertEquiv` `Equiv.invFun` `supportGetEquiv`	—	—
`getVert_surjective` 📖	mathematical	`SimpleGraph.Walk.IsHamiltonian`	`SimpleGraph.Walk.getVert`	—	`Function.Surjective.of_comp` `Function.Bijective.surjective` `SimpleGraph.Walk.isHamiltonian_iff_support_get_bijective` `SimpleGraph.Walk.getVert_comp_val_eq_get_support`
`isPath` 📖	mathematical	`SimpleGraph.Walk.IsHamiltonian`	`SimpleGraph.Walk.IsPath`	—	`SimpleGraph.Walk.IsPath.mk'` `List.nodup_iff_count_le_one` `le_of_eq`
`length_eq` 📖	mathematical	`SimpleGraph.Walk.IsHamiltonian`	`SimpleGraph.Walk.length` `Fintype.card`	—	`eq_tsub_of_add_eq` `Nat.instOrderedSub` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `SimpleGraph.Walk.length_support` `List.sum_toFinset_count_eq_length` `Finset.sum_congr` `Finset.card_eq_sum_ones` `support_toFinset` `Finset.card_univ`
`length_support` 📖	mathematical	`SimpleGraph.Walk.IsHamiltonian`	`SimpleGraph.Walk.support` `Fintype.card`	—	—
`map` 📖	mathematical	`Function.Bijective` `DFunLike.coe` `SimpleGraph.Hom` `RelHom.instFunLike` `SimpleGraph.Adj` `SimpleGraph.Walk.IsHamiltonian`	`SimpleGraph.Walk.map`	—	`SimpleGraph.Walk.support_map` `Function.Surjective.forall` `Function.Bijective.surjective` `List.count_map_of_injective` `Function.Bijective.injective`
`mem_support` 📖	mathematical	`SimpleGraph.Walk.IsHamiltonian`	`SimpleGraph.Walk.support`	—	—
`of_subsingleton` 📖	mathematical	—	`SimpleGraph.Walk.IsHamiltonian`	—	`SimpleGraph.Walk.nil_iff_support_eq` `SimpleGraph.Walk.nil_of_subsingleton`
`supportGetEquiv_apply` 📖	mathematical	`SimpleGraph.Walk.IsHamiltonian`	`DFunLike.coe` `Equiv` `SimpleGraph.Walk.support` `EquivLike.toFunLike` `Equiv.instEquivLike` `supportGetEquiv`	—	—
`supportGetEquiv_symm_apply_val` 📖	mathematical	`SimpleGraph.Walk.IsHamiltonian`	`SimpleGraph.Walk.support` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `supportGetEquiv`	—	—
`support_toFinset` 📖	mathematical	`SimpleGraph.Walk.IsHamiltonian`	`List.toFinset` `SimpleGraph.Walk.support` `Finset.univ`	—	—

SimpleGraph.Walk.IsHamiltonianCycle

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`count_support_self` 📖	mathematical	`SimpleGraph.Walk.IsHamiltonianCycle`	`SimpleGraph.Walk.support`	—	`SimpleGraph.Walk.support_eq_cons` `SimpleGraph.Walk.support_tail_of_not_nil` `SimpleGraph.Walk.IsCycle.not_nil` `toIsCycle` `isHamiltonian_tail`
`isCycle` 📖	mathematical	`SimpleGraph.Walk.IsHamiltonianCycle`	`SimpleGraph.Walk.IsCycle`	—	`toIsCycle`
`isHamiltonian_tail` 📖	mathematical	`SimpleGraph.Walk.IsHamiltonianCycle`	`SimpleGraph.Walk.IsHamiltonian` `SimpleGraph.Walk.snd` `SimpleGraph.Walk.tail`	—	—
`length_eq` 📖	mathematical	`SimpleGraph.Walk.IsHamiltonianCycle`	`SimpleGraph.Walk.length` `Fintype.card`	—	`SimpleGraph.Walk.length_tail_add_one` `SimpleGraph.Walk.IsCycle.not_nil` `toIsCycle` `SimpleGraph.Walk.IsHamiltonian.length_eq` `isHamiltonian_tail` `Fintype.card_pos_iff`
`map` 📖	mathematical	`Function.Bijective` `DFunLike.coe` `SimpleGraph.Hom` `RelHom.instFunLike` `SimpleGraph.Adj` `SimpleGraph.Walk.IsHamiltonianCycle`	`SimpleGraph.Walk.map`	—	`SimpleGraph.Walk.IsCycle.map` `Function.Bijective.injective` `isCycle` `Function.Surjective.forall` `Function.Bijective.surjective` `SimpleGraph.Walk.IsCircuit.ne_nil` `SimpleGraph.Walk.IsCycle.isCircuit` `toIsCycle` `SimpleGraph.Walk.getVert_zero` `SimpleGraph.Walk.tail_cons` `SimpleGraph.Hom.map_adj` `SimpleGraph.Walk.support_copy` `SimpleGraph.Walk.support_map` `List.count_map_of_injective` `isHamiltonian_tail`
`mem_support` 📖	mathematical	`SimpleGraph.Walk.IsHamiltonianCycle`	`SimpleGraph.Walk.support`	—	`SimpleGraph.Walk.IsHamiltonian.mem_support` `isHamiltonian_tail` `SimpleGraph.Walk.support_tail_of_not_nil` `SimpleGraph.Walk.IsCycle.not_nil` `toIsCycle`
`support_count_of_ne` 📖	mathematical	`SimpleGraph.Walk.IsHamiltonianCycle`	`SimpleGraph.Walk.support`	—	`SimpleGraph.Walk.cons_support_tail` `SimpleGraph.Walk.IsCycle.not_nil` `toIsCycle` `isHamiltonian_tail`
`toIsCycle` 📖	mathematical	`SimpleGraph.Walk.IsHamiltonianCycle`	`SimpleGraph.Walk.IsCycle`	—	—

SimpleGraph.Walk.IsPath

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isHamiltonian_iff` 📖	mathematical	`SimpleGraph.Walk.IsPath`	`SimpleGraph.Walk.IsHamiltonian` `SimpleGraph.Walk.support`	—	`SimpleGraph.Walk.IsHamiltonian.mem_support` `isHamiltonian_of_mem`
`isHamiltonian_of_mem` 📖	mathematical	`SimpleGraph.Walk.IsPath` `SimpleGraph.Walk.support`	`SimpleGraph.Walk.IsHamiltonian`	—	`le_antisymm` `List.nodup_iff_count_le_one` `support_nodup`

---

← Back to Index