Documentation Verification Report

UniversalVerts

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

Statistics

Metric	Count
Definitions `deleteUniversalVerts`, `universalVerts`	2
Theorems `exists_of_universalVerts`, `deleteUniversalVerts_adj`, `deleteUniversalVerts_verts`, `disjoint_image_val_universalVerts`, `even_ncard_image_val_supp_sdiff_image_val_rep_union`, `isClique_universalVerts`	6
Total	8

SimpleGraph

Definitions

Name	Category	Theorems
`deleteUniversalVerts` 📖	CompOp	3 math math: `deleteUniversalVerts_verts`, `disjoint_image_val_universalVerts`, `deleteUniversalVerts_adj`
`universalVerts` 📖	CompOp	4 math math: `deleteUniversalVerts_verts`, `disjoint_image_val_universalVerts`, `isClique_universalVerts`, `deleteUniversalVerts_adj`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`deleteUniversalVerts_adj` 📖	mathematical	—	`Subgraph.Adj` `deleteUniversalVerts` `Set` `Set.instMembership` `universalVerts` `Adj`	—	—
`deleteUniversalVerts_verts` 📖	mathematical	—	`Subgraph.verts` `deleteUniversalVerts` `Set` `Set.instSDiff` `Set.univ` `universalVerts`	—	—
`disjoint_image_val_universalVerts` 📖	mathematical	—	`Disjoint` `Set` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `Set.image` `Set.instMembership` `Subgraph.verts` `deleteUniversalVerts` `universalVerts`	—	`Set.image_congr` `Set.compl_eq_univ_diff` `sdiff_sdiff_right_self` `inf_of_le_right` `sdiff_self` `Subtype.coe_image_subset`
`even_ncard_image_val_supp_sdiff_image_val_rep_union` 📖	mathematical	`Set` `Set.instHasSubset` `universalVerts` `ConnectedComponent.Represents` `Set.Elem` `Subgraph.verts` `deleteUniversalVerts` `Subgraph.coe` `oddComponents`	`Even` `Set.ncard` `Set.instSDiff` `Set.image` `Set.instMembership` `ConnectedComponent.supp` `Set.instUnion`	—	`Set.image_diff` `Subtype.val_injective` `sdiff_eq_left` `Set.disjoint_of_subset_right` `disjoint_image_val_universalVerts` `Set.image_inter` `Set.inter_diff_distrib_right` `Set.inter_self` `Set.diff_inter_self_eq_diff` `Set.ncard_image_of_injective` `ConnectedComponent.even_ncard_supp_sdiff_rep`
`isClique_universalVerts` 📖	mathematical	—	`IsClique` `universalVerts`	—	—

SimpleGraph.Subgraph.IsMatching

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_of_universalVerts` 📖	mathematical	`Disjoint` `Set` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `SimpleGraph.universalVerts` `Set.ncard`	`Set.instHasSubset` `SimpleGraph.Subgraph.verts` `Set.instUnion` `SimpleGraph.Subgraph.IsMatching`	—	`Set.exists_subset_card_eq` `Cardinal.eq` `Set.cast_ncard` `Set.toFinite` `Subtype.finite` `Disjoint.ne_of_mem` `Set.disjoint_of_subset_left` `exists_of_disjoint_sets_of_equiv` `Disjoint.symm`

---

← Back to Index