VertexCover

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

Statistics

Metric	Count
Definitions `IsVertexCover`, `vertexCoverNum`	2
Theorems `vertexCoverNum_le_vertexCoverNum`, `mono`, `preimage`, `subset`, `vertexCoverNum_le`, `exists_of_le_vertexCoverNum`, `isIndepSet_compl_iff_isVertexCover`, `isVertexCover_bot`, `isVertexCover_compl`, `isVertexCover_empty`, `isVertexCover_image_iso`, `isVertexCover_preimage_iso`, `isVertexCover_univ`, `vertexCoverNum_bot`, `vertexCoverNum_congr`, `vertexCoverNum_eq_zero`, `vertexCoverNum_exists`, `vertexCoverNum_le_card_sub_one`, `vertexCoverNum_le_encard_edgeSet`, `vertexCoverNum_le_iff`, `vertexCoverNum_le_vertexCoverNum_of_injective`, `vertexCoverNum_lt_card`, `vertexCoverNum_mono`, `vertexCoverNum_ne_top_of_finite`, `vertexCoverNum_ne_top_of_finite_edgeSet`, `vertexCoverNum_of_subsingleton`, `vertexCoverNum_top`	27
Total	29

SimpleGraph

Definitions

Name	Category	Theorems
`IsVertexCover` 📖	MathDef	9 math math: `isVertexCover_preimage_iso`, `isVertexCover_bot`, `isVertexCover_image_iso`, `isIndepSet_compl_iff_isVertexCover`, `vertexCoverNum_exists`, `isVertexCover_univ`, `isVertexCover_compl`, `exists_of_le_vertexCoverNum`, `isVertexCover_empty`
`vertexCoverNum` 📖	CompOp	14 math math: `vertexCoverNum_le_card_sub_one`, `vertexCoverNum_le_iff`, `vertexCoverNum_congr`, `vertexCoverNum_le_vertexCoverNum_of_injective`, `vertexCoverNum_top`, `vertexCoverNum_mono`, `vertexCoverNum_le_encard_edgeSet`, `vertexCoverNum_lt_card`, `vertexCoverNum_eq_zero`, `IsVertexCover.vertexCoverNum_le`, `vertexCoverNum_of_subsingleton`, `vertexCoverNum_exists`, `vertexCoverNum_bot`, `IsContained.vertexCoverNum_le_vertexCoverNum`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_of_le_vertexCoverNum` 📖	mathematical	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `vertexCoverNum` `ENat.instNatCast` `ENat.card`	`Set.encard` `IsVertexCover`	—	`vertexCoverNum_exists` `Set.exists_superset_subset_encard_eq` `Set.encard_univ` `IsVertexCover.subset`
`isIndepSet_compl_iff_isVertexCover` 📖	mathematical	—	`IsIndepSet` `Compl.compl` `Set` `Set.instCompl` `IsVertexCover`	—	`Adj.ne`
`isVertexCover_bot` 📖	mathematical	—	`IsVertexCover` `Bot.bot` `SimpleGraph` `BooleanAlgebra.toBot` `CompleteBooleanAlgebra.toBooleanAlgebra` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `completeAtomicBooleanAlgebra`	—	`instIsEmptyFalse`
`isVertexCover_compl` 📖	mathematical	—	`IsVertexCover` `Compl.compl` `Set` `Set.instCompl` `IsIndepSet`	—	`compl_compl`
`isVertexCover_empty` 📖	mathematical	—	`IsVertexCover` `Set` `Set.instEmptyCollection` `Bot.bot` `SimpleGraph` `BooleanAlgebra.toBot` `CompleteBooleanAlgebra.toBooleanAlgebra` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `completeAtomicBooleanAlgebra`	—	—
`isVertexCover_image_iso` 📖	mathematical	—	`IsVertexCover` `Set.image` `DFunLike.coe` `Iso` `RelIso.instFunLike` `Adj`	—	`RelIso.image_eq_preimage_symm`
`isVertexCover_preimage_iso` 📖	mathematical	—	`IsVertexCover` `Set.preimage` `DFunLike.coe` `Iso` `RelIso.instFunLike` `Adj`	—	`Set.image_preimage_eq` `RelIso.surjective` `IsVertexCover.preimage` `RelIso.instRelHomClass`
`isVertexCover_univ` 📖	mathematical	—	`IsVertexCover` `Set.univ`	—	—
`vertexCoverNum_bot` 📖	mathematical	—	`vertexCoverNum` `emptyGraph` `ENat` `instZeroENat`	—	`nonpos_iff_eq_zero` `IsVertexCover.vertexCoverNum_le` `Set.encard_empty`
`vertexCoverNum_congr` 📖	mathematical	—	`vertexCoverNum`	—	`le_antisymm` `IsContained.vertexCoverNum_le_vertexCoverNum` `Iso.isContained`
`vertexCoverNum_eq_zero` 📖	mathematical	—	`vertexCoverNum` `ENat` `instZeroENat` `Bot.bot` `SimpleGraph` `BooleanAlgebra.toBot` `CompleteBooleanAlgebra.toBooleanAlgebra` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `completeAtomicBooleanAlgebra`	—	`vertexCoverNum_exists` `vertexCoverNum_bot`
`vertexCoverNum_exists` 📖	mathematical	—	`Set.encard` `vertexCoverNum` `IsVertexCover`	—	`nonempty_subtype` `ENat.exists_eq_iInf` `iInf_subtype`
`vertexCoverNum_le_card_sub_one` 📖	mathematical	—	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `vertexCoverNum` `instSubENat` `ENat.card` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat`	—	`Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim` `vertexCoverNum_of_subsingleton` `Nontrivial.to_nonempty` `not_subsingleton_iff_nontrivial` `not_subsingleton` `ENat.forall_natCast_le_iff_le` `Set.encard_diff_singleton_of_mem` `Set.mem_univ` `Set.encard_univ`
`vertexCoverNum_le_encard_edgeSet` 📖	mathematical	—	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `vertexCoverNum` `Set.encard` `Sym2` `edgeSet`	—	`edgeSet_eq_empty` `edgeSet_bot` `vertexCoverNum_bot` `Set.encard_empty` `ENat.forall_natCast_le_iff_le`
`vertexCoverNum_le_iff` 📖	mathematical	—	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `vertexCoverNum`	—	—
`vertexCoverNum_le_vertexCoverNum_of_injective` 📖	mathematical	`DFunLike.coe` `Hom` `RelHom.instFunLike` `Adj`	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `vertexCoverNum`	—	`IsContained.vertexCoverNum_le_vertexCoverNum`
`vertexCoverNum_lt_card` 📖	mathematical	—	`ENat` `Preorder.toLT` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `vertexCoverNum` `ENat.card`	—	`ENat.add_one_le_iff` `vertexCoverNum_ne_top_of_finite` `le_imp_le_of_le_of_le` `add_le_add_left` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `vertexCoverNum_le_card_sub_one` `le_refl` `ENat.card_eq_coe_natCard` `Order.one_le_iff_pos` `Nat.instZeroLEOneClass` `Nat.card_pos`
`vertexCoverNum_mono` 📖	mathematical	`SimpleGraph` `instLE`	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `vertexCoverNum`	—	`IsContained.vertexCoverNum_le_vertexCoverNum` `IsContained.of_le`
`vertexCoverNum_ne_top_of_finite` 📖	—	—	—	—	`ne_top_of_le_ne_top` `vertexCoverNum_le_card_sub_one`
`vertexCoverNum_ne_top_of_finite_edgeSet` 📖	—	—	—	—	`ne_top_of_le_ne_top` `Set.encard_ne_top_iff` `vertexCoverNum_le_encard_edgeSet`
`vertexCoverNum_of_subsingleton` 📖	mathematical	—	`vertexCoverNum` `ENat` `instZeroENat`	—	`subsingleton_iff` `vertexCoverNum_bot`
`vertexCoverNum_top` 📖	mathematical	—	`vertexCoverNum` `completeGraph` `ENat` `instSubENat` `ENat.card` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat`	—	`Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim` `vertexCoverNum_of_subsingleton` `tsub_eq_zero_of_le` `ENat.eq_of_forall_natCast_le_iff` `le_imp_le_of_le_of_le` `le_refl` `vertexCoverNum_le_card_sub_one` `tsub_le_iff_right` `Nat.instAtLeastTwoHAddOfNat` `add_assoc` `one_add_one_eq_two` `exists_of_le_vertexCoverNum` `ENat.le_sub_one_of_lt` `ENat.add_one_le_iff` `Set.encard_diff` `Set.finite_of_encard_eq_coe` `Set.encard_univ` `ENat.le_sub_of_add_le_left` `Nat.cast_one` `add_le_of_le_tsub_right_of_le` `CanonicallyOrderedAdd.toExistsAddOfLE` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `Order.add_one_le_of_lt` `ENat.one_lt_card` `ENat.coe_sub` `tsub_le_tsub` `Set.one_lt_encard_iff`

SimpleGraph.IsContained

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`vertexCoverNum_le_vertexCoverNum` 📖	mathematical	—	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `SimpleGraph.vertexCoverNum`	—	`SimpleGraph.vertexCoverNum_exists` `SimpleGraph.isIndepSet_iff_isAntichain_adj` `SimpleGraph.isIndepSet_compl_iff_isVertexCover` `IsAntichain.preimage` `RelHom.map_rel'` `le_imp_le_of_le_of_le` `SimpleGraph.IsVertexCover.vertexCoverNum_le` `le_refl` `Function.Embedding.encard_le`

SimpleGraph.IsVertexCover

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mono` 📖	—	`SimpleGraph` `SimpleGraph.instLE` `SimpleGraph.IsVertexCover`	—	—	—
`preimage` 📖	mathematical	`SimpleGraph.IsVertexCover`	`Set.preimage` `DFunLike.coe`	—	`RelHomClass.map_rel`
`subset` 📖	—	`Set` `Set.instHasSubset` `SimpleGraph.IsVertexCover`	—	—	—
`vertexCoverNum_le` 📖	mathematical	`SimpleGraph.IsVertexCover`	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `SimpleGraph.vertexCoverNum` `Set.encard`	—	`SimpleGraph.vertexCoverNum_le_iff`

---

← Back to Index