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	12 math math: isVertexCover_preimage_iso, IsVertexCover.mono, isVertexCover_bot, isVertexCover_image_iso, IsVertexCover.subset, isIndepSet_compl_iff_isVertexCover, vertexCoverNum_exists, isVertexCover_univ, IsVertexCover.preimage, 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 instLEENat vertexCoverNum ENat.instNatCast ENat.card	Set Set.encard ENat ENat.instNatCast 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 MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat	—	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 MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat Bot.bot SimpleGraph BooleanAlgebra.toBot CompleteBooleanAlgebra.toBooleanAlgebra CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra completeAtomicBooleanAlgebra	—	vertexCoverNum_exists vertexCoverNum_bot
vertexCoverNum_exists 📖	mathematical	—	Set Set.encard vertexCoverNum IsVertexCover	—	nonempty_subtype ENat.exists_eq_iInf iInf_subtype
vertexCoverNum_le_card_sub_one 📖	mathematical	—	ENat instLEENat vertexCoverNum instSubENat ENat.card AddMonoidWithOne.toOne instAddMonoidWithOneENat	—	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 instLEENat vertexCoverNum Set.encard Sym2 edgeSet	—	edgeSet_eq_empty edgeSet_bot vertexCoverNum_bot Set.encard_empty instReflLe ENat.forall_natCast_le_iff_le
vertexCoverNum_le_iff 📖	mathematical	—	ENat instLEENat vertexCoverNum	—	—
vertexCoverNum_le_vertexCoverNum_of_injective 📖	mathematical	DFunLike.coe Hom RelHom.instFunLike Adj	ENat instLEENat vertexCoverNum	—	IsContained.vertexCoverNum_le_vertexCoverNum
vertexCoverNum_lt_card 📖	mathematical	—	ENat instLTENat 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 instLEENat 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 MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat	—	subsingleton_iff vertexCoverNum_bot
vertexCoverNum_top 📖	mathematical	—	vertexCoverNum completeGraph ENat instSubENat ENat.card AddMonoidWithOne.toOne instAddMonoidWithOneENat	—	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 instLEENat 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 📖	mathematical	SimpleGraph SimpleGraph.instLE SimpleGraph.IsVertexCover	SimpleGraph.IsVertexCover	—	—
preimage 📖	mathematical	SimpleGraph.IsVertexCover	SimpleGraph.IsVertexCover Set.preimage DFunLike.coe	—	RelHomClass.map_rel
subset 📖	mathematical	Set Set.instHasSubset SimpleGraph.IsVertexCover	SimpleGraph.IsVertexCover	—	—
vertexCoverNum_le 📖	mathematical	SimpleGraph.IsVertexCover	ENat instLEENat SimpleGraph.vertexCoverNum Set.encard	—	SimpleGraph.vertexCoverNum_le_iff

---

← Back to Index