Defs

📁 Source: Mathlib/Combinatorics/SimpleGraph/Ends/Defs.lean

Statistics

Metric	Count
Definitions `ComponentCompl`, `coeGraph`, `hom`, `setLike`, `supp`, `componentComplFunctor`, `componentComplMk`, `end`, `instPartialOrderComponentCompl`	9
Theorems `coe_inj`, `disjoint_right`, `exists_adj_boundary_pair`, `exists_eq_mk`, `hom_eq_iff_le`, `hom_eq_iff_not_disjoint`, `hom_infinite`, `hom_mk`, `hom_refl`, `hom_trans`, `ind`, `infinite_iff_in_all_ranges`, `mem_of_adj`, `mem_supp_iff`, `nonempty`, `notMem_of_mem`, `subset_hom`, `supp_inj`, `supp_injective`, `supp_injective_iff`, `componentComplFunctor_map`, `componentComplFunctor_obj`, `componentComplMk_eq_of_adj`, `componentComplMk_mem`, `componentComplMk_mem_hom`, `componentCompl_finite`, `componentCompl_nonempty_of_infinite`, `end_hom_mk_of_mk`, `infinite_iff_in_eventualRange`	29
Total	38

SimpleGraph

Definitions

Name	Category	Theorems
`ComponentCompl` 📖	CompOp	15 math math: `ComponentCompl.subset_hom`, `ComponentCompl.disjoint_right`, `ComponentCompl.pairwise_disjoint`, `componentComplFunctor_obj`, `componentComplMk_mem`, `ComponentCompl.supp_injective`, `ComponentCompl.coe_inj`, `componentCompl_finite`, `ComponentCompl.hom_eq_iff_not_disjoint`, `ComponentCompl.mem_supp_iff`, `ComponentCompl.hom_eq_iff_le`, `ComponentCompl.nonempty`, `componentComplMk_mem_hom`, `ComponentCompl.exists_adj_boundary_pair`, `componentCompl_nonempty_of_infinite`
`componentComplFunctor` 📖	CompOp	5 math math: `componentComplFunctor_obj`, `infinite_iff_in_eventualRange`, `componentComplFunctor_finite`, `componentComplFunctor_nonempty_of_infinite`, `componentComplFunctor_map`
`componentComplMk` 📖	CompOp	6 math math: `ComponentCompl.hom_mk`, `componentComplMk_mem`, `componentComplMk_eq_of_adj`, `ComponentCompl.exists_eq_mk`, `ComponentCompl.mem_supp_iff`, `componentComplMk_mem_hom`
`end` 📖	CompOp	3 math math: `instIsEmptyElemForallObjOppositeFinsetComponentComplFunctorEndOfFinite`, `end_componentCompl_infinite`, `nonempty_ends_of_infinite`
`instPartialOrderComponentCompl` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`componentComplFunctor_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `Opposite` `Finset` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `Finset.partialOrder` `CategoryTheory.types` `componentComplFunctor` `ComponentCompl.hom` `SetLike.coe` `Finset.instSetLike` `Opposite.unop`	—	—
`componentComplFunctor_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `Opposite` `Finset` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `Finset.partialOrder` `CategoryTheory.types` `componentComplFunctor` `ComponentCompl` `SetLike.coe` `Finset.instSetLike` `Opposite.unop`	—	—
`componentComplMk_eq_of_adj` 📖	mathematical	`Set` `Set.instMembership` `Adj`	`componentComplMk`	—	`ConnectedComponent.eq` `Adj.reachable`
`componentComplMk_mem` 📖	mathematical	`Set` `Set.instMembership`	`ComponentCompl` `SetLike.instMembership` `ComponentCompl.setLike` `componentComplMk`	—	—
`componentComplMk_mem_hom` 📖	mathematical	`Set` `Set.instMembership` `Set.instHasSubset`	`ComponentCompl` `SetLike.instMembership` `ComponentCompl.setLike` `ComponentCompl.hom` `componentComplMk`	—	`ComponentCompl.subset_hom` `componentComplMk_mem`
`componentCompl_finite` 📖	mathematical	—	`Finite` `ComponentCompl` `SetLike.coe` `Finset` `Finset.instSetLike`	—	`Finset.eq_empty_or_nonempty` `Finset.coe_empty` `Set.compl_empty` `Preconnected.subsingleton_connectedComponent` `Fact.out` `Finite.of_equiv` `Finite.of_subsingleton` `ComponentCompl.exists_adj_boundary_pair` `Adj.symm` `Pairwise.eq` `ComponentCompl.pairwise_disjoint` `Set.not_disjoint_iff` `Subtype.finite` `Set.Finite.to_subtype` `Set.Finite.ofFinset` `Finite.of_injective_finite_range`
`componentCompl_nonempty_of_infinite` 📖	mathematical	—	`ComponentCompl` `SetLike.coe` `Finset` `Finset.instSetLike`	—	`Set.Infinite.nonempty` `Set.Finite.infinite_compl` `Finset.finite_toSet`
`end_hom_mk_of_mk` 📖	mathematical	`Set` `Set.instMembership` `end` `Finset` `Finset.instMembership` `Opposite.unop` `componentComplMk` `Multiset` `Multiset.instMembership` `Finset.val`	`SetLike.coe` `Finset.instSetLike` `Set.notMem_subset` `CategoryTheory.le_of_op_hom` `PartialOrder.toPreorder` `Finset.partialOrder`	—	`Set.notMem_subset` `CategoryTheory.le_of_op_hom`
`infinite_iff_in_eventualRange` 📖	mathematical	—	`Set.Infinite` `ComponentCompl.supp` `SetLike.coe` `Finset` `Finset.instSetLike` `Opposite.unop` `CategoryTheory.Functor.obj` `Opposite` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `Finset.partialOrder` `CategoryTheory.types` `componentComplFunctor` `Set` `Set.instMembership` `CategoryTheory.Functor.eventualRange`	—	`ComponentCompl.infinite_iff_in_all_ranges` `CategoryTheory.le_of_op_hom`

SimpleGraph.ComponentCompl

Definitions

Name	Category	Theorems
`coeGraph` 📖	CompOp	—
`hom` 📖	CompOp	10 math math: `subset_hom`, `hom_mk`, `hom_trans`, `hom_refl`, `hom_infinite`, `hom_eq_iff_not_disjoint`, `infinite_iff_in_all_ranges`, `hom_eq_iff_le`, `SimpleGraph.componentComplMk_mem_hom`, `SimpleGraph.componentComplFunctor_map`
`setLike` 📖	CompOp	11 math math: `subset_hom`, `disjoint_right`, `pairwise_disjoint`, `SimpleGraph.componentComplMk_mem`, `coe_inj`, `hom_eq_iff_not_disjoint`, `mem_supp_iff`, `hom_eq_iff_le`, `nonempty`, `SimpleGraph.componentComplMk_mem_hom`, `exists_adj_boundary_pair`
`supp` 📖	CompOp	6 math math: `SimpleGraph.infinite_iff_in_eventualRange`, `SimpleGraph.end_componentCompl_infinite`, `supp_inj`, `supp_injective`, `supp_injective_iff`, `infinite_iff_in_all_ranges`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_inj` 📖	mathematical	—	`SetLike.coe` `SimpleGraph.ComponentCompl` `setLike`	—	`SetLike.coe_set_eq`
`disjoint_right` 📖	mathematical	—	`Disjoint` `Set` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `SetLike.coe` `SimpleGraph.ComponentCompl` `setLike`	—	`Set.disjoint_iff`
`exists_adj_boundary_pair` 📖	mathematical	`SimpleGraph.Preconnected` `Set.Nonempty`	`SimpleGraph.ComponentCompl` `SetLike.instMembership` `setLike` `Set` `Set.instMembership` `SimpleGraph.Adj`	—	`ind` `Set.disjoint_iff` `disjoint_right` `Set.eq_univ_iff_forall` `SimpleGraph.Walk.exists_boundary_dart` `SimpleGraph.componentComplMk_mem` `mem_of_adj` `Mathlib.Tactic.Push.not_and_eq` `Set.mem_univ`
`exists_eq_mk` 📖	mathematical	—	`SimpleGraph.componentComplMk`	—	`nonempty`
`hom_eq_iff_le` 📖	mathematical	`Set` `Set.instHasSubset`	`hom` `SetLike.coe` `SimpleGraph.ComponentCompl` `setLike`	—	`subset_hom` `ind`
`hom_eq_iff_not_disjoint` 📖	mathematical	`Set` `Set.instHasSubset`	`hom` `Disjoint` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `SetLike.coe` `SimpleGraph.ComponentCompl` `setLike`	—	`Set.not_disjoint_iff` `ind`
`hom_infinite` 📖	mathematical	`Set` `Set.instHasSubset` `Set.Infinite` `SetLike.coe` `SimpleGraph.ComponentCompl` `setLike`	`hom`	—	`Set.Infinite.mono` `subset_hom`
`hom_mk` 📖	mathematical	`Set` `Set.instMembership` `Set.instHasSubset`	`hom` `SimpleGraph.componentComplMk` `Set.notMem_subset`	—	—
`hom_refl` 📖	mathematical	—	`hom` `subset_refl` `Set` `Set.instHasSubset` `Set.instReflSubset`	—	`subset_refl` `Set.instReflSubset` `Set.mapsTo_id` `SimpleGraph.induceHom_id` `SimpleGraph.ConnectedComponent.map_id`
`hom_trans` 📖	mathematical	`Set` `Set.instHasSubset`	`hom` `HasSubset.Subset.trans` `Set.instIsTransSubset`	—	`HasSubset.Subset.trans` `Set.instIsTransSubset` `SimpleGraph.ConnectedComponent.map_comp` `Set.MapsTo.comp` `SimpleGraph.induceHom_comp`
`ind` 📖	—	`SimpleGraph.componentComplMk`	—	—	`SimpleGraph.ConnectedComponent.ind`
`infinite_iff_in_all_ranges` 📖	mathematical	—	`Set.Infinite` `supp` `SetLike.coe` `Finset` `Finset.instSetLike` `hom` `Multiset` `Multiset.instMembership` `Finset.val`	—	`Set.Infinite.nonempty` `Set.Infinite.diff` `Finset.finite_toSet` `Finset.subset_union_left` `nonempty` `disjoint_right` `Set.Finite.coe_toFinset` `Finset.coe_union` `hom_eq_iff_le`
`mem_of_adj` 📖	—	`SimpleGraph.ComponentCompl` `SetLike.instMembership` `setLike` `Set` `Set.instMembership` `SimpleGraph.Adj`	—	—	`SimpleGraph.ConnectedComponent.eq` `SimpleGraph.Adj.reachable` `SimpleGraph.Adj.symm`
`mem_supp_iff` 📖	mathematical	—	`SimpleGraph.ComponentCompl` `SetLike.instMembership` `setLike` `SimpleGraph.componentComplMk`	—	—
`nonempty` 📖	mathematical	—	`Set.Nonempty` `SetLike.coe` `SimpleGraph.ComponentCompl` `setLike`	—	`ind`
`notMem_of_mem` 📖	mathematical	`SimpleGraph.ComponentCompl` `SetLike.instMembership` `setLike`	`Set` `Set.instMembership`	—	`Set.disjoint_iff` `disjoint_right`
`subset_hom` 📖	mathematical	`Set` `Set.instHasSubset`	`SetLike.coe` `SimpleGraph.ComponentCompl` `setLike` `hom`	—	—
`supp_inj` 📖	mathematical	—	`supp`	—	`supp_injective`
`supp_injective` 📖	mathematical	—	`SimpleGraph.ComponentCompl` `Set` `supp`	—	`SimpleGraph.ConnectedComponent.ind₂` `SimpleGraph.Reachable.refl`
`supp_injective_iff` 📖	mathematical	—	`supp`	—	`supp_injective`

---

← Back to Index