Documentation Verification Report

Acyclic

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

Statistics

Metric	Count
Definitions `Acyclic`, `IsAcyclic`, `coloringTwo`, `coloringTwoOfVerts`, `IsTree`, `coloringTwo`, `coloringTwoOfVert`	7
Theorems `card_vert_le_card_edgeSet_add_one`, `exists_connected_induce_compl_singleton_of_finite_nontrivial`, `exists_isTree_le`, `exists_isTree_le_of_le_of_isAcyclic`, `exists_preconnected_induce_compl_singleton_of_finite`, `induce_compl_singleton_of_degree_eq_one`, `maximal_le_isAcyclic_iff_isTree`, `anti`, `comap`, `dist_eq_dist_add_one_of_adj_of_reachable`, `dist_ne_of_adj`, `embedding`, `induce`, `isBipartite`, `isPath_iff_isChain`, `isPath_iff_isTrail`, `isTree_connectedComponent`, `mem_support_of_ne_mem_support_of_adj_of_isPath`, `ne_mem_support_of_support_of_adj_of_isPath`, `of_comap`, `of_map`, `of_subsingleton`, `path_concat`, `path_unique`, `subgraph`, `IsAcyclic`, `card_edgeFinset`, `coe_singletonSubgraph`, `coe_subgraphOfAdj`, `dist_eq_dist_add_one_of_adj`, `dist_ne_of_adj`, `existsUnique_path`, `exists_vert_degree_one_of_nontrivial`, `isBipartite`, `isConnected`, `minDegree_eq_one_of_nontrivial`, `of_subsingleton`, `isAcyclic_iff`, `isTree_iff`, `isAcyclic_coe_bot`, `exists_isAcyclic_reachable_eq_le`, `exists_isAcyclic_reachable_eq_le_of_le_of_isAcyclic`, `exists_maximal_isAcyclic_of_le_isAcyclic`, `isAcyclic_add_edge_iff_of_not_reachable`, `isAcyclic_bot`, `isAcyclic_iff_forall_adj_isBridge`, `isAcyclic_iff_forall_edge_isBridge`, `isAcyclic_iff_path_unique`, `isAcyclic_of_path_unique`, `isAcyclic_sSup_of_isAcyclic_directedOn`, `isTree_iff`, `isTree_iff_connected_and_card`, `isTree_iff_existsUnique_path`, `isTree_iff_minimal_connected`, `isTree_of_minimal_connected`, `maximal_isAcyclic_iff_isTree`, `maximal_isAcyclic_iff_reachable_eq`, `reachable_eq_of_maximal_isAcyclic`	58
Total	65

HomologicalComplex

Definitions

Name	Category	Theorems
`Acyclic` 📖	MathDef	6 math math: `acyclic_of_isZero`, `acyclic_truncGE_iff_isSupportedOutside`, `acyclic_op_iff`, `HomotopyCategory.quotient_obj_mem_subcategoryAcyclic_iff_acyclic`, `acyclic_iff`, `acyclic_truncLE_iff_isSupportedOutside`

SimpleGraph

Definitions

Name	Category	Theorems
`IsAcyclic` 📖	MathDef	18 math math: `isAcyclic_of_path_unique`, `exists_girth_eq_length`, `isAcyclic_iff_forall_adj_isBridge`, `girth_eq_zero`, `IsAcyclic.of_subsingleton`, `isTree_iff`, `exists_egirth_eq_length`, `Connected.maximal_le_isAcyclic_iff_isTree`, `Subgraph.isAcyclic_coe_bot`, `egirth_eq_top`, `isAcyclic_iff_forall_edge_isBridge`, `Iso.isAcyclic_iff`, `maximal_isAcyclic_iff_isTree`, `isAcyclic_add_edge_iff_of_not_reachable`, `IsTree.IsAcyclic`, `isAcyclic_bot`, `isAcyclic_iff_path_unique`, `exists_isAcyclic_reachable_eq_le`
`IsTree` 📖	CompData	14 math math: `Connected.exists_isTree_le_of_le_of_isAcyclic`, `isTree_iff_existsUnique_path`, `isTree_iff`, `Iso.isTree_iff`, `isTree_iff_minimal_connected`, `IsTree.coe_subgraphOfAdj`, `Connected.maximal_le_isAcyclic_iff_isTree`, `isTree_iff_connected_and_card`, `Connected.exists_isTree_le`, `IsTree.coe_singletonSubgraph`, `IsAcyclic.isTree_connectedComponent`, `IsTree.of_subsingleton`, `maximal_isAcyclic_iff_isTree`, `isTree_of_minimal_connected`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_isAcyclic_reachable_eq_le` 📖	mathematical	—	`SimpleGraph` `instLE` `IsAcyclic` `Reachable`	—	`exists_isAcyclic_reachable_eq_le_of_le_of_isAcyclic` `bot_le` `isAcyclic_bot`
`exists_isAcyclic_reachable_eq_le_of_le_of_isAcyclic` 📖	mathematical	`SimpleGraph` `instLE` `IsAcyclic`	`Reachable`	—	`exists_maximal_isAcyclic_of_le_isAcyclic`
`exists_maximal_isAcyclic_of_le_isAcyclic` 📖	mathematical	`SimpleGraph` `instLE` `IsAcyclic`	`Maximal`	—	`zorn_le_nonempty₀` `isAcyclic_sSup_of_isAcyclic_directedOn` `IsChain.directedOn` `instReflLe` `CompleteLattice.le_sSup`
`isAcyclic_add_edge_iff_of_not_reachable` 📖	mathematical	`Reachable`	`IsAcyclic` `SimpleGraph` `instMax` `fromEdgeSet` `Sym2` `Set` `Set.instSingletonSet`	—	`IsAcyclic.anti` `le_sup_left` `Reachable.refl` `sup_sdiff_right_self` `Adj.reachable` `isBridge_iff_adj_and_forall_cycle_notMem` `edgeSet_sup` `edgeSet_fromEdgeSet` `Walk.edges_subset_edgeSet` `Walk.IsCycle.transfer`
`isAcyclic_bot` 📖	mathematical	—	`IsAcyclic` `Bot.bot` `SimpleGraph` `BooleanAlgebra.toBot` `CompleteBooleanAlgebra.toBooleanAlgebra` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `completeAtomicBooleanAlgebra`	—	`Walk.IsCycle.ne_bot`
`isAcyclic_iff_forall_adj_isBridge` 📖	mathematical	—	`IsAcyclic` `IsBridge`	—	`Walk.IsCycle.not_of_nil` `Walk.edges_cons`
`isAcyclic_iff_forall_edge_isBridge` 📖	mathematical	—	`IsAcyclic` `IsBridge`	—	—
`isAcyclic_iff_path_unique` 📖	mathematical	—	`IsAcyclic`	—	`IsAcyclic.path_unique` `isAcyclic_of_path_unique`
`isAcyclic_of_path_unique` 📖	mathematical	—	`IsAcyclic`	—	`Adj.symm` `Path.singleton.eq_1` `Walk.cons.congr_simp`
`isAcyclic_sSup_of_isAcyclic_directedOn` 📖	mathematical	`IsAcyclic` `DirectedOn` `SimpleGraph` `instLE`	`SupSet.sSup` `supSet`	—	`Set.eq_empty_or_nonempty` `sSup_empty` `Walk.IsCycle.transfer`
`isTree_iff` 📖	mathematical	—	`IsTree` `Connected` `IsAcyclic`	—	—
`isTree_iff_connected_and_card` 📖	mathematical	—	`IsTree` `Connected` `Nat.card` `Set.Elem` `Sym2` `edgeSet`	—	`IsTree.isConnected` `Nat.card_eq_fintype_card` `Fintype.card_ofFinset` `Set.toFinset_card` `IsTree.card_edgeFinset` `by_contra` `LE.le.not_gt` `Connected.card_vert_le_card_edgeSet_add_one` `Connected.connected_delete_edge_of_not_isBridge` `edgeFinset_card` `add_lt_add_iff_right` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `contravariant_swap_add_of_contravariant_add` `contravariant_lt_of_covariant_le` `Finset.card_lt_card` `Set.toFinset_congr` `edgeSet_sdiff` `edgeSet_fromEdgeSet` `edgeSet_sdiff_sdiff_isDiag` `Set.toFinset_diff` `Set.toFinset_singleton` `Finset.coe_sdiff` `Set.coe_toFinset` `Finset.coe_singleton`
`isTree_iff_existsUnique_path` 📖	mathematical	—	`IsTree` `ExistsUnique` `Walk` `Walk.IsPath`	—	`isTree_iff` `isAcyclic_iff_path_unique` `Connected.nonempty` `Connected.preconnected` `Walk.reachable` `ExistsUnique.unique`
`isTree_iff_minimal_connected` 📖	mathematical	—	`IsTree` `Minimal` `SimpleGraph` `instLE` `Connected`	—	`IsTree.isConnected` `Connected.exists_isPath` `Walk.IsPath.mapLe` `IsAcyclic.path_unique` `IsTree.IsAcyclic` `Walk.adj_of_mem_edges` `Walk.edges_map` `Sym2.map_id` `isTree_of_minimal_connected`
`isTree_of_minimal_connected` 📖	mathematical	`Minimal` `SimpleGraph` `instLE` `Connected`	`IsTree`	—	`isTree_iff` `Minimal.prop` `isAcyclic_iff_forall_adj_isBridge` `by_contra` `Minimal.not_prop_of_lt` `edgeSet_sdiff` `edgeSet_fromEdgeSet` `edgeSet_sdiff_sdiff_isDiag` `Connected.connected_delete_edge_of_not_isBridge`
`maximal_isAcyclic_iff_isTree` 📖	mathematical	—	`Maximal` `SimpleGraph` `instLE` `IsAcyclic` `IsTree`	—	`Connected.maximal_le_isAcyclic_iff_isTree` `connected_top` `le_top`
`maximal_isAcyclic_iff_reachable_eq` 📖	mathematical	`SimpleGraph` `instLE` `IsAcyclic`	`Maximal` `Reachable`	—	`reachable_eq_of_maximal_isAcyclic` `exists_gt_of_not_maximal` `Set.exists_of_ssubset` `edgeSet_strict_mono` `IsAcyclic.anti` `sup_le_iff` `fromEdgeSet_edgeSet` `sup_sdiff_right_self` `isAcyclic_iff_forall_edge_isBridge` `edgeSet_sup` `edgeSet_fromEdgeSet` `not_isDiag_of_mem_edgeSet` `Sym2.ind` `Reachable.mono` `Adj.reachable`
`reachable_eq_of_maximal_isAcyclic` 📖	mathematical	`Maximal` `SimpleGraph` `instLE` `IsAcyclic`	`Reachable`	—	`Maximal.prop` `Maximal.le_of_ge` `Reachable.mono` `Mathlib.Tactic.Contrapose.contrapose₁` `Mathlib.Tactic.Push.not_forall_eq` `ConnectedComponent.connectedComponentMk_mem` `ConnectedComponent.reachable_of_mem_supp` `Walk.exists_boundary_dart` `ConnectedComponent.eq` `isAcyclic_add_edge_iff_of_not_reachable` `symm` `le_sup_left` `le_iff_adj` `Adj.ne` `ConnectedComponent.mem_supp_congr_adj`

SimpleGraph.Connected

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_vert_le_card_edgeSet_add_one` 📖	mathematical	`SimpleGraph.Connected`	`Nat.card` `Set.Elem` `Sym2` `SimpleGraph.edgeSet`	—	`finite_or_infinite` `Nat.card_eq_zero_of_infinite` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT` `AddRightCancelSemigroup.toIsRightCancelAdd` `contravariant_swap_add_of_contravariant_add` `contravariant_lt_of_covariant_le` `Nat.instCanonicallyOrderedAdd` `exists_isTree_le` `Nat.card_eq_fintype_card` `Subtype.finite` `Quot.finite` `Finite.instProd` `SimpleGraph.IsTree.card_edgeFinset` `add_le_add_iff_right` `SimpleGraph.edgeFinset_card` `Finset.card_mono`
`exists_connected_induce_compl_singleton_of_finite_nontrivial` 📖	mathematical	`SimpleGraph.Connected`	`Set.Elem` `Compl.compl` `Set` `Set.instCompl` `Set.instSingletonSet` `SimpleGraph.induce`	—	`exists_isTree_le` `SimpleGraph.IsTree.exists_vert_degree_one_of_nontrivial` `mono` `induce_compl_singleton_of_degree_eq_one`
`exists_isTree_le` 📖	mathematical	`SimpleGraph.Connected`	`SimpleGraph` `SimpleGraph.instLE` `SimpleGraph.IsTree`	—	`SimpleGraph.exists_isAcyclic_reachable_eq_le_of_le_of_isAcyclic` `bot_le` `SimpleGraph.isAcyclic_bot`
`exists_isTree_le_of_le_of_isAcyclic` 📖	mathematical	`SimpleGraph.Connected` `SimpleGraph` `SimpleGraph.instLE` `SimpleGraph.IsAcyclic`	`SimpleGraph.IsTree`	—	`SimpleGraph.exists_isAcyclic_reachable_eq_le_of_le_of_isAcyclic`
`exists_preconnected_induce_compl_singleton_of_finite` 📖	mathematical	`SimpleGraph.Connected`	`SimpleGraph.Preconnected` `Set.Elem` `Compl.compl` `Set` `Set.instCompl` `Set.instSingletonSet` `SimpleGraph.induce`	—	`Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim` `Set.subsingleton_coe_of_subsingleton` `nonempty` `exists_connected_induce_compl_singleton_of_finite_nontrivial` `preconnected`
`induce_compl_singleton_of_degree_eq_one` 📖	mathematical	`SimpleGraph.Connected` `SimpleGraph.degree`	`Set.Elem` `Compl.compl` `Set` `Set.instCompl` `Set.instSingletonSet` `SimpleGraph.induce`	—	`SimpleGraph.degree_eq_one_iff_existsUnique_adj` `SimpleGraph.connected_iff` `exists_isPath` `SimpleGraph.Reachable.eq_1` `exists_true_iff_nonempty` `Set.mem_compl_iff` `Set.mem_singleton_iff` `SimpleGraph.Walk.mem_support_iff_exists_append` `SimpleGraph.Walk.start_mem_support` `List.nodup_iff_forall_not_duplicate` `SimpleGraph.Path.nodup_support` `SimpleGraph.Walk.support_append` `List.duplicate_iff_two_le_count` `SimpleGraph.Walk.getVert_mem_support` `SimpleGraph.Walk.snd_mem_tail_support` `SimpleGraph.Walk.not_nil_of_ne` `SimpleGraph.Adj.symm` `SimpleGraph.Walk.adj_penultimate` `SimpleGraph.Walk.adj_snd` `SimpleGraph.Walk.end_mem_support` `SetCoe.ext`
`maximal_le_isAcyclic_iff_isTree` 📖	mathematical	`SimpleGraph.Connected` `SimpleGraph` `SimpleGraph.instLE`	`Maximal` `SimpleGraph.IsAcyclic` `SimpleGraph.IsTree`	—	`nonempty` `SimpleGraph.reachable_eq_of_maximal_isAcyclic` `preconnected` `SimpleGraph.maximal_isAcyclic_iff_reachable_eq` `SimpleGraph.IsTree.IsAcyclic` `SimpleGraph.preconnected_iff_reachable_eq_top` `SimpleGraph.IsTree.isConnected`

SimpleGraph.IsAcyclic

Definitions

Name	Category	Theorems
`coloringTwo` 📖	CompOp	—
`coloringTwoOfVerts` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`anti` 📖	—	`SimpleGraph` `SimpleGraph.instLE` `SimpleGraph.IsAcyclic`	—	—	`comap`
`comap` 📖	—	`DFunLike.coe` `SimpleGraph.Hom` `RelHom.instFunLike` `SimpleGraph.Adj` `SimpleGraph.IsAcyclic`	—	—	`Iff.not` `SimpleGraph.Walk.map_isCycle_iff_of_injective`
`dist_eq_dist_add_one_of_adj_of_reachable` 📖	mathematical	`SimpleGraph.IsAcyclic` `SimpleGraph.Adj`	`SimpleGraph.dist`	—	—
`dist_ne_of_adj` 📖	—	`SimpleGraph.IsAcyclic` `SimpleGraph.Adj`	—	—	`SimpleGraph.Reachable.exists_path_of_dist` `SimpleGraph.Reachable.trans` `SimpleGraph.Adj.reachable` `SimpleGraph.Adj.symm` `path_concat` `SimpleGraph.Walk.length_concat` `mem_support_of_ne_mem_support_of_adj_of_isPath`
`embedding` 📖	—	`SimpleGraph.IsAcyclic`	—	—	`comap` `RelEmbedding.injective`
`induce` 📖	mathematical	`SimpleGraph.IsAcyclic`	`Set.Elem` `SimpleGraph.induce`	—	`of_comap`
`isBipartite` 📖	mathematical	`SimpleGraph.IsAcyclic`	`SimpleGraph.IsBipartite`	—	—
`isPath_iff_isChain` 📖	mathematical	`SimpleGraph.IsAcyclic`	`SimpleGraph.Walk.IsPath` `Sym2` `SimpleGraph.Walk.edges`	—	`SimpleGraph.Walk.edges_nodup_of_support_nodup` `SimpleGraph.Walk.isPath_def` `List.isChain_cons` `SimpleGraph.Walk.edges_cons` `SimpleGraph.Walk.cons_isPath_iff` `SimpleGraph.Walk.nil_iff_support_eq` `SimpleGraph.Walk.nil_iff_length_eq` `SimpleGraph.Adj.ne` `SimpleGraph.Walk.take_spec` `SimpleGraph.Walk.adj_snd` `SimpleGraph.Walk.cons_tail_eq` `SimpleGraph.Walk.IsPath.eq_snd_of_mem_edges` `SimpleGraph.Walk.IsPath.mk'` `Sym2.eq_swap` `SimpleGraph.Walk.snd_takeUntil`
`isPath_iff_isTrail` 📖	mathematical	`SimpleGraph.IsAcyclic`	`SimpleGraph.Walk.IsPath` `SimpleGraph.Walk.IsTrail`	—	`SimpleGraph.Walk.IsPath.isTrail` `isPath_iff_isChain` `SimpleGraph.Walk.isTrail_def`
`isTree_connectedComponent` 📖	mathematical	`SimpleGraph.IsAcyclic`	`SimpleGraph.IsTree` `SimpleGraph.ConnectedComponent` `SetLike.instMembership` `SimpleGraph.ConnectedComponent.instSetLike` `SimpleGraph.ConnectedComponent.toSimpleGraph`	—	`SimpleGraph.ConnectedComponent.connected_toSimpleGraph` `comap`
`mem_support_of_ne_mem_support_of_adj_of_isPath` 📖	—	`SimpleGraph.IsAcyclic` `SimpleGraph.Walk.IsPath` `SimpleGraph.Adj` `SimpleGraph.Walk.support`	—	—	`SimpleGraph.Adj.symm` `SimpleGraph.Walk.IsPath.concat` `SimpleGraph.isAcyclic_iff_path_unique` `SimpleGraph.Walk.support_subset_support_concat` `SimpleGraph.Walk.end_mem_support`
`ne_mem_support_of_support_of_adj_of_isPath` 📖	—	`SimpleGraph.IsAcyclic` `SimpleGraph.Walk.IsPath` `SimpleGraph.Adj` `SimpleGraph.Walk.support`	—	—	`SimpleGraph.Walk.IsPath.mem_support_iff_exists_append` `path_unique` `SimpleGraph.Walk.IsPath.ne_of_mem_support_of_append` `SimpleGraph.Adj.ne'` `SimpleGraph.Adj.symm` `SimpleGraph.Walk.end_mem_support`
`of_comap` 📖	mathematical	`SimpleGraph.IsAcyclic`	`SimpleGraph.comap` `DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding`	—	`embedding`
`of_map` 📖	—	`SimpleGraph.IsAcyclic` `SimpleGraph.map`	—	—	`embedding`
`of_subsingleton` 📖	mathematical	—	`SimpleGraph.IsAcyclic`	—	`SimpleGraph.Walk.IsCircuit.ne_nil` `SimpleGraph.Walk.IsCycle.isCircuit` `SimpleGraph.irrefl`
`path_concat` 📖	mathematical	`SimpleGraph.IsAcyclic` `SimpleGraph.Walk.IsPath` `SimpleGraph.Adj` `SimpleGraph.Walk.support`	`SimpleGraph.Walk.concat`	—	`ne_mem_support_of_support_of_adj_of_isPath` `SimpleGraph.Adj.symm` `SimpleGraph.Walk.IsPath.concat` `SimpleGraph.isAcyclic_iff_path_unique`
`path_unique` 📖	—	`SimpleGraph.IsAcyclic`	—	—	`SimpleGraph.Walk.isPath_iff_eq_nil` `SimpleGraph.isBridge_iff_adj_and_forall_walk_mem_edges` `SimpleGraph.isAcyclic_iff_forall_adj_isBridge` `SimpleGraph.Walk.edges_append` `SimpleGraph.Walk.edges_reverse` `SimpleGraph.Walk.cons_isPath_iff` `SimpleGraph.Walk.fst_mem_support_of_mem_edges`
`subgraph` 📖	mathematical	`SimpleGraph.IsAcyclic`	`Set.Elem` `SimpleGraph.Subgraph.verts` `SimpleGraph.Subgraph.coe`	—	`comap` `SimpleGraph.Subgraph.hom_injective`

SimpleGraph.IsTree

Definitions

Name	Category	Theorems
`coloringTwo` 📖	CompOp	—
`coloringTwoOfVert` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`IsAcyclic` 📖	mathematical	`SimpleGraph.IsTree`	`SimpleGraph.IsAcyclic`	—	—
`card_edgeFinset` 📖	mathematical	`SimpleGraph.IsTree`	`Finset.card` `Sym2` `SimpleGraph.edgeFinset` `Fintype.card`	—	`SimpleGraph.Connected.nonempty` `isConnected` `Finset.card_compl` `Finset.card_singleton` `Fintype.card_pos` `AddRightCancelSemigroup.toIsRightCancelAdd` `Finset.card_bij` `SimpleGraph.Walk.not_nil_of_ne` `SimpleGraph.dart_edge_eq_iff` `SimpleGraph.Walk.IsPath.tail` `SimpleGraph.Walk.length_tail_add_one` `SimpleGraph.Walk.length_copy` `le_of_not_ge` `zero_add` `Nat.instCanonicallyOrderedAdd` `SimpleGraph.Walk.length_nil` `SimpleGraph.Walk.length_cons` `SimpleGraph.Walk.IsPath.cons` `SimpleGraph.Walk.IsPath.nil` `SimpleGraph.Adj.ne` `SimpleGraph.dart_edge_eq_mk'_iff` `SimpleGraph.Adj.symm` `SimpleGraph.Walk.cons_isPath_iff` `ExistsUnique.unique` `existsUnique_path` `SimpleGraph.Walk.IsPath.takeUntil` `SimpleGraph.Walk.IsPath.dropUntil` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `SimpleGraph.Walk.take_spec` `SimpleGraph.Walk.getVert_zero` `Sym2.eq_swap`
`coe_singletonSubgraph` 📖	mathematical	—	`SimpleGraph.IsTree` `Set.Elem` `SimpleGraph.Subgraph.verts` `SimpleGraph.singletonSubgraph` `SimpleGraph.Subgraph.coe`	—	`of_subsingleton` `SimpleGraph.nonempty_singletonSubgraph_verts` `Unique.instSubsingleton`
`coe_subgraphOfAdj` 📖	mathematical	`SimpleGraph.Adj`	`SimpleGraph.IsTree` `Set.Elem` `SimpleGraph.Subgraph.verts` `SimpleGraph.subgraphOfAdj` `SimpleGraph.Subgraph.coe`	—	`SimpleGraph.Subgraph.Connected.coe` `SimpleGraph.Subgraph.subgraphOfAdj_connected` `SimpleGraph.Walk.adj_snd` `Iff.not` `SimpleGraph.Walk.nil_iff_eq_nil` `SimpleGraph.Walk.IsCircuit.ne_nil` `SimpleGraph.Walk.IsCycle.isCircuit` `SimpleGraph.Walk.adj_penultimate`
`dist_eq_dist_add_one_of_adj` 📖	mathematical	`SimpleGraph.IsTree` `SimpleGraph.Adj`	`SimpleGraph.dist`	—	—
`dist_ne_of_adj` 📖	—	`SimpleGraph.IsTree` `SimpleGraph.Adj`	—	—	`SimpleGraph.IsAcyclic.dist_ne_of_adj` `IsAcyclic` `SimpleGraph.Connected.preconnected` `isConnected`
`existsUnique_path` 📖	mathematical	`SimpleGraph.IsTree`	`ExistsUnique` `SimpleGraph.Walk` `SimpleGraph.Walk.IsPath`	—	`SimpleGraph.isTree_iff_existsUnique_path`
`exists_vert_degree_one_of_nontrivial` 📖	mathematical	`SimpleGraph.IsTree`	`SimpleGraph.degree` `SimpleGraph.neighborSetFintype`	—	`SimpleGraph.exists_minimal_degree_vertex` `Nontrivial.to_nonempty` `minDegree_eq_one_of_nontrivial`
`isBipartite` 📖	mathematical	`SimpleGraph.IsTree`	`SimpleGraph.IsBipartite`	—	—
`isConnected` 📖	mathematical	`SimpleGraph.IsTree`	`SimpleGraph.Connected`	—	—
`minDegree_eq_one_of_nontrivial` 📖	mathematical	`SimpleGraph.IsTree`	`SimpleGraph.minDegree`	—	`card_edgeFinset` `SimpleGraph.sum_degrees_eq_twice_card_edges` `Finset.sum_le_sum` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `le_trans` `SimpleGraph.minDegree_le_degree` `smul_eq_mul` `Finset.card_univ` `Finset.sum_const` `SimpleGraph.Preconnected.minDegree_pos_of_nontrivial` `SimpleGraph.Connected.preconnected` `isConnected`
`of_subsingleton` 📖	mathematical	—	`SimpleGraph.IsTree`	—	`SimpleGraph.Connected.of_subsingleton` `SimpleGraph.IsAcyclic.of_subsingleton`

SimpleGraph.Iso

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isAcyclic_iff` 📖	mathematical	—	`SimpleGraph.IsAcyclic`	—	`SimpleGraph.IsAcyclic.embedding`
`isTree_iff` 📖	mathematical	—	`SimpleGraph.IsTree`	—	`connected_iff` `isAcyclic_iff`

SimpleGraph.Subgraph

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isAcyclic_coe_bot` 📖	mathematical	—	`SimpleGraph.IsAcyclic` `Set.Elem` `verts` `Bot.bot` `SimpleGraph.Subgraph` `instBot` `coe`	—	`SimpleGraph.IsAcyclic.of_subsingleton` `IsEmpty.instSubsingleton` `Set.isEmpty_coe_sort`

---

← Back to Index