Documentation Verification Report

Finsubgraph

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

Statistics

Metric	Count
Definitions `Finsubgraph`, `instCompl`, `instCompletelyDistribLattice`, `instGeneralizedCoheytingAlgebra`, `instHImp`, `instHNot`, `instInfSet`, `instMax`, `instMin`, `instOrderBot`, `instSDiff`, `instSupSet`, `instTop`, `FinsubgraphHom`, `restrict`, `finsubgraphHomFunctor`, `finsubgraphOfAdj`, `singletonFinsubgraph`	18
Theorems `coe_bot`, `coe_compl`, `coe_himp`, `coe_hnot`, `coe_iInf`, `coe_iSup`, `coe_inf`, `coe_sInf`, `coe_sSup`, `coe_sdiff`, `coe_sup`, `coe_top`, `nonempty_hom_of_forall_finite_subgraph_hom`, `singletonFinsubgraph_le_adj_left`, `singletonFinsubgraph_le_adj_right`	15
Total	33

SimpleGraph

Definitions

Name	Category	Theorems
`Finsubgraph` 📖	CompOp	14 math math: `Finsubgraph.coe_sSup`, `Finsubgraph.coe_top`, `Finsubgraph.coe_hnot`, `Finsubgraph.coe_sdiff`, `Finsubgraph.coe_iInf`, `Finsubgraph.coe_bot`, `Finsubgraph.coe_iSup`, `Finsubgraph.coe_sup`, `Finsubgraph.coe_inf`, `Finsubgraph.coe_himp`, `singletonFinsubgraph_le_adj_left`, `Finsubgraph.coe_sInf`, `Finsubgraph.coe_compl`, `singletonFinsubgraph_le_adj_right`
`FinsubgraphHom` 📖	CompOp	—
`finsubgraphHomFunctor` 📖	CompOp	—
`finsubgraphOfAdj` 📖	CompOp	2 math math: `singletonFinsubgraph_le_adj_left`, `singletonFinsubgraph_le_adj_right`
`singletonFinsubgraph` 📖	CompOp	2 math math: `singletonFinsubgraph_le_adj_left`, `singletonFinsubgraph_le_adj_right`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`nonempty_hom_of_forall_finite_subgraph_hom` 📖	mathematical	—	`Hom`	—	`nonempty_fintype` `nonempty_sections_of_finite_inverse_system` `SemilatticeSup.instIsDirectedOrder` `Finite.of_fintype` `RelHom.coe_fn_injective` `singletonFinsubgraph_le_adj_left` `singletonFinsubgraph_le_adj_right` `Hom.map_adj`
`singletonFinsubgraph_le_adj_left` 📖	mathematical	`Adj`	`Finsubgraph` `Subgraph` `Preorder.toLE` `PartialOrder.toPreorder` `Subgraph.instPartialOrder` `Set.Finite` `Subgraph.verts` `singletonFinsubgraph` `finsubgraphOfAdj`	—	—
`singletonFinsubgraph_le_adj_right` 📖	mathematical	`Adj`	`Finsubgraph` `Subgraph` `Preorder.toLE` `PartialOrder.toPreorder` `Subgraph.instPartialOrder` `Set.Finite` `Subgraph.verts` `singletonFinsubgraph` `finsubgraphOfAdj`	—	—

SimpleGraph.Finsubgraph

Definitions

Name	Category	Theorems
`instCompl` 📖	CompOp	1 math math: `coe_compl`
`instCompletelyDistribLattice` 📖	CompOp	—
`instGeneralizedCoheytingAlgebra` 📖	CompOp	—
`instHImp` 📖	CompOp	1 math math: `coe_himp`
`instHNot` 📖	CompOp	1 math math: `coe_hnot`
`instInfSet` 📖	CompOp	2 math math: `coe_iInf`, `coe_sInf`
`instMax` 📖	CompOp	1 math math: `coe_sup`
`instMin` 📖	CompOp	1 math math: `coe_inf`
`instOrderBot` 📖	CompOp	1 math math: `coe_bot`
`instSDiff` 📖	CompOp	1 math math: `coe_sdiff`
`instSupSet` 📖	CompOp	2 math math: `coe_sSup`, `coe_iSup`
`instTop` 📖	CompOp	1 math math: `coe_top`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_bot` 📖	mathematical	—	`SimpleGraph.Subgraph` `Set.Finite` `SimpleGraph.Subgraph.verts` `Bot.bot` `SimpleGraph.Finsubgraph` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SimpleGraph.Subgraph.instPartialOrder` `instOrderBot` `SimpleGraph.Subgraph.instBot`	—	—
`coe_compl` 📖	mathematical	—	`SimpleGraph.Subgraph` `Set.Finite` `SimpleGraph.Subgraph.verts` `Compl.compl` `SimpleGraph.Finsubgraph` `instCompl` `HeytingAlgebra.toCompl` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompletelyDistribLattice.toCompleteDistribLattice` `SimpleGraph.Subgraph.instCompletelyDistribLattice`	—	—
`coe_himp` 📖	mathematical	—	`SimpleGraph.Subgraph` `Set.Finite` `SimpleGraph.Subgraph.verts` `HImp.himp` `SimpleGraph.Finsubgraph` `instHImp` `GeneralizedHeytingAlgebra.toHImp` `HeytingAlgebra.toGeneralizedHeytingAlgebra` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompletelyDistribLattice.toCompleteDistribLattice` `SimpleGraph.Subgraph.instCompletelyDistribLattice`	—	—
`coe_hnot` 📖	mathematical	—	`SimpleGraph.Subgraph` `Set.Finite` `SimpleGraph.Subgraph.verts` `HNot.hnot` `SimpleGraph.Finsubgraph` `instHNot` `BiheytingAlgebra.toHNot` `CompletelyDistribLattice.toBiheytingAlgebra` `SimpleGraph.Subgraph.instCompletelyDistribLattice`	—	—
`coe_iInf` 📖	mathematical	—	`SimpleGraph.Subgraph` `Set.Finite` `SimpleGraph.Subgraph.verts` `iInf` `SimpleGraph.Finsubgraph` `instInfSet` `SimpleGraph.Subgraph.instInfSet`	—	`iInf.eq_1` `coe_sInf` `iInf_range`
`coe_iSup` 📖	mathematical	—	`SimpleGraph.Subgraph` `Set.Finite` `SimpleGraph.Subgraph.verts` `iSup` `SimpleGraph.Finsubgraph` `instSupSet` `SimpleGraph.Subgraph.instSupSet`	—	`iSup.eq_1` `coe_sSup` `iSup_range`
`coe_inf` 📖	mathematical	—	`SimpleGraph.Subgraph` `Set.Finite` `SimpleGraph.Subgraph.verts` `SimpleGraph.Finsubgraph` `instMin` `SimpleGraph.Subgraph.instMin`	—	—
`coe_sInf` 📖	mathematical	—	`SimpleGraph.Subgraph` `Set.Finite` `SimpleGraph.Subgraph.verts` `InfSet.sInf` `SimpleGraph.Finsubgraph` `instInfSet` `iInf` `SimpleGraph.Subgraph.instInfSet` `Set` `Set.instMembership`	—	—
`coe_sSup` 📖	mathematical	—	`SimpleGraph.Subgraph` `Set.Finite` `SimpleGraph.Subgraph.verts` `SupSet.sSup` `SimpleGraph.Finsubgraph` `instSupSet` `iSup` `SimpleGraph.Subgraph.instSupSet` `Set` `Set.instMembership`	—	—
`coe_sdiff` 📖	mathematical	—	`SimpleGraph.Subgraph` `Set.Finite` `SimpleGraph.Subgraph.verts` `SimpleGraph.Finsubgraph` `instSDiff` `BiheytingAlgebra.toSDiff` `CompletelyDistribLattice.toBiheytingAlgebra` `SimpleGraph.Subgraph.instCompletelyDistribLattice`	—	—
`coe_sup` 📖	mathematical	—	`SimpleGraph.Subgraph` `Set.Finite` `SimpleGraph.Subgraph.verts` `SimpleGraph.Finsubgraph` `instMax` `SimpleGraph.Subgraph.instMax`	—	—
`coe_top` 📖	mathematical	—	`SimpleGraph.Subgraph` `Set.Finite` `SimpleGraph.Subgraph.verts` `Top.top` `SimpleGraph.Finsubgraph` `instTop` `SimpleGraph.Subgraph.instTop`	—	—

SimpleGraph.FinsubgraphHom

Definitions

Name	Category	Theorems
`restrict` 📖	CompOp	—

---

← Back to Index