ENat

📁 Source: Mathlib/Combinatorics/Matroid/Rank/ENat.lean

Statistics

Metric	Count
Definitions eRank, eRk	2
Theorems eRk_lt_encard, eRk_eq_encard, encard_le_eRank, encard_le_eRk_of_subset, exists_insert_of_encard_lt, isBase_of_eRk_ge, isBasis'_of_eRk_ge, isBasis_of_eRk_ge, eRk_eq_eRank, encard_compl_eq, encard_eq_eRank, eRk_eq_eRk, eRk_eq_eRk_insert, eRk_eq_eRk_union, eRk_eq_encard, encard_eq_eRk, eRk_eq_eRk, eRk_eq_eRk_insert, eRk_eq_eRk_union, eRk_eq_encard, encard_eq_eRk, eRk_add_one_eq, eRk_eq, eRk_eq, closure_eq_closure_of_subset_of_eRk_ge_eRk, closure_eq_closure_of_subset_of_forall_insert, eRk_lt_top, indep_of_encard_le_eRk, isBasis_of_subset_closure_of_subset_of_encard_le, eRank_restrict, eRk_eq, eRank_add_eRank_dual, eRank_def, eRank_emptyOn, eRank_eq_top, eRank_eq_top_iff, eRank_eq_zero_iff, eRank_freeOn, eRank_le_encard_add_eRk_compl, eRank_le_encard_ground, eRank_loopyOn, eRank_lt_top_iff, eRank_map, eRank_ne_top_iff, eRank_restrict, eRk_closure_eq, eRk_comap, eRk_compl_insert_union_add_eRk_compl_insert_inter_le, eRk_compl_union_add_eRk_compl_inter_le, eRk_compl_union_of_disjoint, eRk_dual_add_eRank, eRk_dual_add_eRank', eRk_empty, eRk_eq_eRank, eRk_eq_eRk_diff_eRk_le_zero, eRk_eq_eRk_of_subset_of_le, eRk_eq_eRk_union_eRk_le_zero, eRk_eq_of_eRk_insert_le_forall, eRk_eq_one_iff, eRk_eq_top_iff, eRk_eq_zero_iff, eRk_eq_zero_iff', eRk_freeOn, eRk_ground, eRk_ground_inter, eRk_ground_union, eRk_insert_closure_eq, eRk_insert_eq_add_one, eRk_insert_inter_add_eRk_insert_union_le, eRk_insert_le_add_one, eRk_insert_of_notMem_ground, eRk_inter_add_eRk_union_le, eRk_inter_ground, eRk_le_eRank, eRk_le_eRk_add_eRk_diff, eRk_le_eRk_inter_add_eRk_diff, eRk_le_encard, eRk_le_iff, eRk_le_one_iff, eRk_loops, eRk_loopyOn, eRk_lt_encard_iff_dep, eRk_lt_encard_iff_dep_of_finite, eRk_lt_encard_of_dep_of_finite, eRk_lt_top_iff, eRk_map, eRk_mono, eRk_ne_top_iff, eRk_singleton_eq, eRk_singleton_eq_one_iff, eRk_singleton_le, eRk_submod, eRk_union_closure_left_eq, eRk_union_closure_right_eq, eRk_union_ground, eRk_union_le_eRk_add_eRk, eRk_union_le_eRk_add_encard, eRk_union_le_encard_add_eRk, eRk_univ_eq, eq_eRk_iff, eq_loopyOn_iff_eRank, exists_eRk_insert_eq_add_one_of_lt, exists_of_eRank_eq_zero, indep_iff_eRk_eq_encard, indep_iff_eRk_eq_encard_of_finite, isBasis'_iff_indep_encard_eq_of_finite, isBasis_iff_indep_encard_eq_of_finite, le_eRk_iff, one_le_eRank, restrict_eRk_eq, restrict_eRk_eq', spanning_iff_eRk_le, spanning_iff_eRk_le'	113
Total	115

Matroid

Definitions

Name	Category	Theorems
eRank 📖	CompOp	32 math math: IsBase.encard_eq_eRank, eRank_loopyOn, eRank_map, Spanning.eRank_restrict, eRank_le_encard_add_eRk_compl, eRank_freeOn, eRank_eq_top, eRk_dual_add_eRank', eRank_eq_top_iff, eRank_emptyOn, spanning_iff_eRk_le', eRk_union_ground, eRk_dual_add_eRank, eRk_univ_eq, eRank_le_encard_ground, eRank_lt_top_iff, Indep.encard_le_eRank, eRank_def, Spanning.eRk_eq, eRank_restrict, eRk_ground, eRank_eq_zero_iff, eRk_ground_union, eRk_le_eRank, eRank_add_eRank_dual, IsBase.eRk_eq_eRank, eq_loopyOn_iff_eRank, one_le_eRank, toENat_cRank_eq, IsBase.encard_compl_eq, spanning_iff_eRk_le, eRk_eq_eRank
eRk 📖	CompOp	87 math math: eRk_insert_closure_eq, eRk_lt_top_iff, eRk_loops, eRk_lt_encard_iff_dep, eRk_empty, eRk_singleton_le, eRk_mono, eRank_le_encard_add_eRk_compl, Indep.eRk_eq_encard, isBasis_iff_indep_encard_eq_of_finite, le_eRk_iff, IsNonloop.eRk_eq, eRk_union_closure_left_eq, eRk_lt_encard_iff_dep_of_finite, eRk_map, IsBasis.eRk_eq_encard, eRk_dual_add_eRank', eRk_compl_union_of_disjoint, eRk_le_eRk_add_eRk_diff, eRk_eq_eRk_diff_eRk_le_zero, eRk_compl_insert_union_add_eRk_compl_insert_inter_le, IsBasis'.encard_eq_eRk, eRk_insert_le_add_one, spanning_iff_eRk_le', exists_eRk_insert_eq_add_one_of_lt, IsBasis.eRk_eq_eRk_insert, eRk_union_ground, eRk_inter_add_eRk_union_le, IsBasis.encard_eq_eRk, eRk_dual_add_eRank, eRk_eq_eRk_of_subset_of_le, eRk_eq_of_eRk_insert_le_forall, eRk_univ_eq, IsRkFinite.eRk_lt_top, Indep.encard_le_eRk_of_subset, IsBasis'.eRk_eq_encard, eRk_insert_inter_add_eRk_insert_union_le, eRank_def, eRk_inter_ground, IsBasis.eRk_eq_eRk_union, Spanning.eRk_eq, eRank_restrict, eRk_le_iff, eRk_eq_top_iff, eRk_loopyOn, IsLoop.eRk_eq, indep_iff_eRk_eq_encard_of_finite, eRk_ground_inter, eRk_union_le_eRk_add_eRk, eRk_le_eRk_inter_add_eRk_diff, eRk_ground, IsCircuit.eRk_add_one_eq, eRk_eq_one_iff, eRk_ground_union, restrict_eRk_eq', eRk_comap, eRk_eq_zero_iff', IsBasis'.eRk_eq_eRk_union, eRk_le_eRank, restrict_eRk_eq, eRk_eq_zero_iff, eRk_union_closure_right_eq, eRk_lt_encard_of_dep_of_finite, IsBasis.eRk_eq_eRk, indep_iff_eRk_eq_encard, eRk_freeOn, eRk_union_le_encard_add_eRk, eRk_union_le_eRk_add_encard, eRk_insert_eq_add_one, eRk_eq_eRk_union_eRk_le_zero, eRk_singleton_eq, IsBasis'.eRk_eq_eRk, IsBasis'.eRk_eq_eRk_insert, Dep.eRk_lt_encard, eRk_insert_of_notMem_ground, isBasis'_iff_indep_encard_eq_of_finite, eRk_compl_union_add_eRk_compl_inter_le, eq_eRk_iff, IsBase.eRk_eq_eRank, eRk_le_one_iff, eRk_singleton_eq_one_iff, eRk_le_encard, eRk_submod, spanning_iff_eRk_le, eRk_eq_eRank, toENat_cRk_eq, eRk_closure_eq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eRank_add_eRank_dual 📖	mathematical	—	ENat instAddENat eRank dual Set.encard E	—	exists_isBase IsBase.encard_eq_eRank IsBase.compl_isBase_dual Set.encard_union_eq Set.disjoint_sdiff_right Set.union_diff_cancel IsBase.subset_ground
eRank_def 📖	mathematical	—	eRank eRk E	—	eRk.eq_1 restrict_ground_eq_self
eRank_emptyOn 📖	mathematical	—	eRank emptyOn ENat MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat	—	eRank_eq_zero_iff emptyOn_ground loopyOn_empty
eRank_eq_top 📖	mathematical	—	eRank Top.top ENat instTopENat	—	eRank_eq_top_iff
eRank_eq_top_iff 📖	mathematical	—	eRank Top.top ENat instTopENat RankInfinite	—	not_rankFinite_iff eRank_ne_top_iff
eRank_eq_zero_iff 📖	mathematical	—	eRank ENat MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat loopyOn E	—	closure_empty_eq_ground_iff exists_isBase Set.encard_eq_zero IsBase.encard_eq_eRank IsBase.closure_eq eRank_loopyOn
eRank_freeOn 📖	mathematical	—	eRank freeOn Set.encard	—	eRank_def freeOn_ground Indep.eRk_eq_encard freeOn_indep_iff Eq.subset Set.instReflSubset
eRank_le_encard_add_eRk_compl 📖	mathematical	—	ENat instLEENat eRank instAddENat Set.encard eRk Set Set.instSDiff E	—	le_trans eRk_inter_ground eRank_def Set.union_diff_self Set.union_inter_cancel_right le_refl eRk_union_le_encard_add_eRk
eRank_le_encard_ground 📖	mathematical	—	ENat instLEENat eRank Set.encard E	—	Eq.trans_le eRank_def eRk_le_encard
eRank_loopyOn 📖	mathematical	—	eRank loopyOn ENat MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat	—	eRank_def eRk_loopyOn
eRank_lt_top_iff 📖	mathematical	—	ENat instLTENat eRank Top.top instTopENat RankFinite	—	—
eRank_map 📖	mathematical	Set.InjOn E	eRank map	—	exists_isBase IsBase.encard_eq_eRank IsBase.map Set.InjOn.encard_image Set.InjOn.mono IsBase.subset_ground
eRank_ne_top_iff 📖	mathematical	—	RankFinite	—	exists_isBase IsBase.encard_eq_eRank Set.encard_ne_top_iff IsBase.rankFinite_of_finite IsBase.finite
eRank_restrict 📖	mathematical	—	eRank restrict eRk	—	—
eRk_closure_eq 📖	mathematical	—	eRk closure	—	exists_isBasis' IsBasis'.closure_eq_closure IsBasis.encard_eq_eRk Indep.isBasis_closure IsBasis'.indep IsBasis'.encard_eq_eRk
eRk_comap 📖	mathematical	—	eRk comap Set.image	—	exists_isBasis' comap_isBasis'_iff IsBasis'.encard_eq_eRk Set.InjOn.encard_image
eRk_compl_insert_union_add_eRk_compl_insert_inter_le 📖	mathematical	—	ENat instLEENat instAddENat eRk Set Set.instSDiff E Set.instInsert Set.instUnion Set.instInter	—	Set.insert_union_distrib Set.insert_inter_distrib eRk_compl_union_add_eRk_compl_inter_le
eRk_compl_union_add_eRk_compl_inter_le 📖	mathematical	—	ENat instLEENat instAddENat eRk Set Set.instSDiff E Set.instUnion Set.instInter	—	Set.diff_inter_diff Set.diff_inter eRk_submod
eRk_compl_union_of_disjoint 📖	mathematical	Disjoint Set OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice	eRk Set Set.instUnion Set.instSDiff E	—	eRk_inter_ground Set.union_inter_distrib_right Set.inter_eq_self_of_subset_left Set.diff_subset Set.union_eq_self_of_subset_right Set.subset_diff Set.inter_subset_right Disjoint.mono_left Set.inter_subset_left Disjoint.symm
eRk_dual_add_eRank 📖	mathematical	Set Set.instHasSubset E	ENat instAddENat eRk dual eRank Set Set.instSDiff E Set.encard	—	exists_isBasis IsBasis.exists_isBasis_inter_eq_of_superset Set.instReflSubset isBasis_ground_iff dual_dual IsBase.inter_isBasis_iff_compl_inter_isBasis_dual IsBase.encard_eq_eRank IsBase.compl_isBase_of_dual IsBasis.eRk_eq_encard Set.encard_union_eq
eRk_dual_add_eRank' 📖	mathematical	—	ENat instAddENat eRk dual eRank Set Set.instSDiff E Set.encard Set.instInter	—	Set.diff_inter_self_eq_diff eRk_dual_add_eRank dual_ground eRk_inter_ground
eRk_empty 📖	mathematical	—	eRk Set Set.instEmptyCollection ENat MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat	—	IsBasis.encard_eq_eRk Indep.isBasis_self empty_indep Set.encard_empty
eRk_eq_eRank 📖	mathematical	Set Set.instHasSubset E	eRk eRank	—	eRk_inter_ground Set.inter_eq_self_of_subset_right eRank_def
eRk_eq_eRk_diff_eRk_le_zero 📖	mathematical	ENat instLEENat eRk MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat	eRk Set Set.instSDiff	—	eRk_eq_eRk_union_eRk_le_zero Set.diff_union_self
eRk_eq_eRk_of_subset_of_le 📖	mathematical	Set Set.instHasSubset ENat instLEENat eRk	eRk	—	LE.le.antisymm eRk_mono
eRk_eq_eRk_union_eRk_le_zero 📖	mathematical	ENat instLEENat eRk MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat	eRk Set Set.instUnion	—	LE.le.antisymm LE.le.trans_eq LE.le.trans eRk_union_le_eRk_add_eRk add_le_add_right IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid add_zero eRk_mono Set.subset_union_left
eRk_eq_of_eRk_insert_le_forall 📖	mathematical	Set Set.instHasSubset ENat instLEENat eRk Set.instInsert	eRk	—	eRk_closure_eq IsRkFinite.closure_eq_closure_of_subset_of_forall_insert eRk_eq_top_iff IsRkFinite.subset
eRk_eq_one_iff 📖	mathematical	Set Set.instHasSubset E	eRk ENat AddMonoidWithOne.toOne instAddMonoidWithOneENat Set Set.instMembership IsNonloop Set.instHasSubset closure Set.instSingletonSet	—	exists_isBasis IsBasis.eRk_eq_encard Set.encard_eq_one Set.singleton_subset_iff IsBasis.subset indep_singleton IsBasis.indep IsBasis.subset_closure IsNonloop.eRk_eq LE.le.antisymm LE.le.trans eRk_mono Eq.le eRk_closure_eq
eRk_eq_top_iff 📖	mathematical	—	eRk Top.top ENat instTopENat IsRkFinite	—	exists_isBasis' IsBasis'.eRk_eq_encard Set.encard_eq_top_iff IsBasis'.finite_iff_isRkFinite Set.Infinite.eq_1
eRk_eq_zero_iff 📖	mathematical	Set Set.instHasSubset E	eRk ENat MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat Set Set.instHasSubset loops	—	eRk_eq_zero_iff' Set.inter_eq_self_of_subset_left
eRk_eq_zero_iff' 📖	mathematical	—	eRk ENat MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat Set Set.instHasSubset Set.instInter E loops	—	exists_isBasis eRk_inter_ground IsBasis.encard_eq_eRk Set.encard_eq_zero Set.eq_empty_iff_forall_notMem IsNonloop.not_isLoop Indep.isNonloop_of_mem IsBasis.indep IsBasis.subset
eRk_freeOn 📖	mathematical	Set Set.instHasSubset	eRk freeOn Set.encard	—	exists_isBasis IsBasis.eRk_eq_encard Indep.eq_of_isBasis freeOn_indep
eRk_ground 📖	mathematical	—	eRk E eRank	—	eRank_def
eRk_ground_inter 📖	mathematical	—	eRk Set Set.instInter E	—	Set.inter_comm eRk_inter_ground
eRk_ground_union 📖	mathematical	—	eRk Set Set.instUnion E eRank	—	Set.union_comm eRk_union_ground
eRk_insert_closure_eq 📖	mathematical	—	eRk Set Set.instInsert closure	—	Set.union_singleton eRk_union_closure_left_eq
eRk_insert_eq_add_one 📖	mathematical	Set Set.instMembership Set.instSDiff E closure	eRk Set Set.instInsert ENat instAddENat AddMonoidWithOne.toOne instAddMonoidWithOneENat	—	exists_isBasis' eRk_closure_eq closure_insert_congr_right IsBasis'.closure_eq_closure IsBasis'.eRk_eq_encard Indep.eRk_eq_encard Indep.mem_closure_iff' IsBasis'.indep Set.mem_diff Set.encard_insert_of_notMem
eRk_insert_inter_add_eRk_insert_union_le 📖	mathematical	—	ENat instLEENat instAddENat eRk Set Set.instInsert Set.instInter Set.instUnion	—	Set.insert_inter_distrib Set.insert_union_distrib eRk_submod
eRk_insert_le_add_one 📖	mathematical	—	ENat instLEENat eRk Set Set.instInsert instAddENat AddMonoidWithOne.toOne instAddMonoidWithOneENat	—	LE.le.trans eRk_union_le_eRk_add_eRk Set.union_singleton add_le_add_right IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid Set.encard_singleton eRk_le_encard
eRk_insert_of_notMem_ground 📖	mathematical	Set Set.instMembership E	eRk Set Set.instInsert	—	eRk_inter_ground Set.insert_inter_of_notMem
eRk_inter_add_eRk_union_le 📖	mathematical	—	ENat instLEENat instAddENat eRk Set Set.instInter Set.instUnion	—	exists_isBasis' Indep.subset_isBasis'_of_subset IsBasis'.indep HasSubset.Subset.trans Set.instIsTransSubset IsBasis'.subset Set.inter_subset_left Set.inter_subset_right IsBasis'.eRk_eq_eRk_union Set.union_comm IsBasis'.encard_eq_eRk Set.encard_union_add_encard_inter add_comm add_le_add IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid covariant_swap_add_of_covariant_add eRk_le_encard Set.encard_mono Set.subset_inter
eRk_inter_ground 📖	mathematical	—	eRk Set Set.instInter E	—	exists_isBasis' IsBasis'.eRk_eq_eRk IsBasis.eRk_eq_eRk IsBasis'.isBasis_inter_ground
eRk_le_eRank 📖	mathematical	—	ENat instLEENat eRk eRank	—	eRank_def eRk_inter_ground eRk_mono Set.inter_subset_right
eRk_le_eRk_add_eRk_diff 📖	mathematical	Set Set.instHasSubset	ENat instLEENat eRk instAddENat Set Set.instSDiff	—	Set.union_diff_cancel eRk_union_le_eRk_add_eRk
eRk_le_eRk_inter_add_eRk_diff 📖	mathematical	—	ENat instLEENat eRk instAddENat Set Set.instInter Set.instSDiff	—	Set.inter_union_diff eRk_union_le_eRk_add_eRk
eRk_le_encard 📖	mathematical	—	ENat instLEENat eRk Set.encard	—	exists_isBasis' IsBasis'.eRk_eq_encard Set.encard_mono IsBasis'.subset
eRk_le_iff 📖	mathematical	—	ENat instLEENat eRk Set.encard	—	Eq.trans_le Indep.eRk_eq_encard LE.le.trans eRk_mono exists_isBasis' IsBasis'.encard_eq_eRk IsBasis'.subset IsBasis'.indep
eRk_le_one_iff 📖	mathematical	Set Set.instHasSubset E	ENat instLEENat eRk AddMonoidWithOne.toOne instAddMonoidWithOneENat Set Set.instMembership E Set.instHasSubset closure Set.instSingletonSet	—	exists_isBasis Set.encard_le_one_iff_eq IsBasis.eRk_eq_encard ground_nonempty HasSubset.Subset.trans Set.instIsTransSubset IsBasis.subset_closure closure_subset_closure Set.empty_subset Indep.subset_ground IsBasis.indep LE.le.trans eRk_mono eRk_closure_eq Set.encard_singleton eRk_le_encard
eRk_loops 📖	mathematical	—	eRk loops ENat MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat	—	—
eRk_loopyOn 📖	mathematical	—	eRk loopyOn ENat MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat	—	exists_isBasis' IsBasis'.eRk_eq_encard loopyOn_indep_iff IsBasis'.indep Set.encard_empty
eRk_lt_encard_iff_dep 📖	mathematical	Set Set.instHasSubset E	ENat instLTENat eRk Set.encard Dep	—	not_indep_iff LT.lt.ne Indep.eRk_eq_encard Dep.eRk_lt_encard
eRk_lt_encard_iff_dep_of_finite 📖	mathematical	Set Set.instHasSubset E	ENat instLTENat eRk Set.encard Dep	—	not_indep_iff indep_iff_eRk_eq_encard_of_finite LT.lt.ne eRk_lt_encard_of_dep_of_finite
eRk_lt_encard_of_dep_of_finite 📖	mathematical	Dep	ENat instLTENat eRk Set.encard	—	lt_of_le_of_ne eRk_le_encard Indep.not_dep indep_iff_eRk_eq_encard_of_finite
eRk_lt_top_iff 📖	mathematical	—	ENat instLTENat eRk Top.top instTopENat IsRkFinite	—	lt_top_iff_ne_top eRk_ne_top_iff
eRk_map 📖	mathematical	Set.InjOn E Set Set.instHasSubset	eRk map Set.image	—	exists_isBasis IsBasis.eRk_eq_encard IsBasis.map Set.InjOn.encard_image Set.InjOn.mono Indep.subset_ground IsBasis.indep
eRk_mono 📖	mathematical	—	Monotone Set ENat PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra instPreorderENat eRk	—	exists_isBasis' Indep.subset_isBasis'_of_subset IsBasis'.indep HasSubset.Subset.trans Set.instIsTransSubset IsBasis'.subset IsBasis'.eRk_eq_encard Set.encard_mono
eRk_ne_top_iff 📖	mathematical	—	IsRkFinite	—	—
eRk_singleton_eq 📖	mathematical	Set Set.instMembership E	eRk Set Set.instSingletonSet ENat AddMonoidWithOne.toOne instAddMonoidWithOneENat	—	IsNonloop.eRk_eq isNonloop_of_loopless
eRk_singleton_eq_one_iff 📖	mathematical	—	eRk Set Set.instSingletonSet ENat AddMonoidWithOne.toOne instAddMonoidWithOneENat IsNonloop	—	indep_singleton indep_iff_eRk_eq_encard_of_finite Set.encard_singleton IsNonloop.eRk_eq
eRk_singleton_le 📖	mathematical	—	ENat instLEENat eRk Set Set.instSingletonSet AddMonoidWithOne.toOne instAddMonoidWithOneENat	—	LE.le.trans_eq eRk_le_encard Set.encard_singleton
eRk_submod 📖	mathematical	—	ENat instLEENat instAddENat eRk Set Set.instInter Set.instUnion	—	eRk_inter_add_eRk_union_le
eRk_union_closure_left_eq 📖	mathematical	—	eRk Set Set.instUnion closure	—	eRk_closure_eq closure_union_closure_left_eq
eRk_union_closure_right_eq 📖	mathematical	—	eRk Set Set.instUnion closure	—	eRk_closure_eq closure_union_closure_right_eq
eRk_union_ground 📖	mathematical	—	eRk Set Set.instUnion E eRank	—	eRk_inter_ground Set.inter_eq_self_of_subset_right Set.subset_union_right eRank_def
eRk_union_le_eRk_add_eRk 📖	mathematical	—	ENat instLEENat eRk Set Set.instUnion instAddENat	—	LE.le.trans le_add_self eRk_submod
eRk_union_le_eRk_add_encard 📖	mathematical	—	ENat instLEENat eRk Set Set.instUnion instAddENat Set.encard	—	LE.le.trans eRk_union_le_eRk_add_eRk le_imp_le_of_le_of_le le_refl add_le_add_right IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid eRk_le_encard
eRk_union_le_encard_add_eRk 📖	mathematical	—	ENat instLEENat eRk Set Set.instUnion instAddENat Set.encard	—	LE.le.trans eRk_union_le_eRk_add_eRk le_imp_le_of_le_of_le add_le_add_left covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid eRk_le_encard le_refl
eRk_univ_eq 📖	mathematical	—	eRk Set.univ eRank	—	eRk_inter_ground Set.univ_inter eRank_def
eq_eRk_iff 📖	mathematical	Set Set.instHasSubset E	eRk Set IsBasis Set.encard	—	exists_isBasis IsBasis.encard_eq_eRk
eq_loopyOn_iff_eRank 📖	mathematical	—	loopyOn eRank ENat MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat E	—	eRank_loopyOn eRank_eq_zero_iff
exists_eRk_insert_eq_add_one_of_lt 📖	mathematical	ENat instLTENat eRk	Set Set.instMembership Set.instSDiff eRk Set.instInsert ENat instAddENat AddMonoidWithOne.toOne instAddMonoidWithOneENat	—	Mathlib.Tactic.Contrapose.contrapose₃ eRk_inter_ground eRk_closure_eq eRk_mono Set.not_subset mem_closure_of_mem' eRk_insert_eq_add_one
exists_of_eRank_eq_zero 📖	mathematical	eRank ENat MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat	Set loopyOn	—	—
indep_iff_eRk_eq_encard 📖	mathematical	—	Indep eRk Set.encard	—	Indep.eRk_eq_encard Set.finite_or_infinite indep_iff_eRk_eq_encard_of_finite LT.lt.ne IsRkFinite.eRk_lt_top isRkFinite_set Set.Infinite.encard_eq
indep_iff_eRk_eq_encard_of_finite 📖	mathematical	—	Indep eRk Set.encard	—	Indep.eRk_eq_encard exists_isBasis' Set.Finite.eq_of_subset_of_encard_le' IsBasis'.subset IsBasis'.eRk_eq_encard le_refl IsBasis'.indep
isBasis'_iff_indep_encard_eq_of_finite 📖	mathematical	—	IsBasis' Set Set.instHasSubset Indep Set.encard eRk	—	IsBasis'.subset IsBasis'.indep IsBasis'.eRk_eq_encard Indep.subset_isBasis'_of_subset Set.Finite.eq_of_subset_of_encard_le Eq.le IsBasis'.encard_eq_eRk
isBasis_iff_indep_encard_eq_of_finite 📖	mathematical	Set Set.instHasSubset E	IsBasis Set Set.instHasSubset Indep Set.encard eRk	—	isBasis'_iff_isBasis isBasis'_iff_indep_encard_eq_of_finite
le_eRk_iff 📖	mathematical	—	ENat instLEENat eRk Set Set.instHasSubset Indep Set.encard	—	exists_isBasis' Set.exists_subset_encard_eq IsBasis'.encard_eq_eRk HasSubset.Subset.trans Set.instIsTransSubset IsBasis'.subset Indep.subset IsBasis'.indep Indep.eRk_eq_encard eRk_mono
one_le_eRank 📖	mathematical	—	ENat instLEENat AddMonoidWithOne.toOne instAddMonoidWithOneENat eRank	—	exists_isBase IsBase.encard_eq_eRank Set.one_le_encard_iff_nonempty IsBase.nonempty
restrict_eRk_eq 📖	mathematical	Set Set.instHasSubset	eRk restrict	—	restrict_eRk_eq' Set.inter_eq_self_of_subset_left
restrict_eRk_eq' 📖	mathematical	—	eRk restrict Set Set.instInter	—	exists_isBasis' IsBasis'.eRk_eq_encard eRk_inter_ground IsBasis.eRk_eq_encard restrict_ground_eq isBasis_restrict_iff' isBasis'_iff_isBasis_inter_ground
spanning_iff_eRk_le 📖	mathematical	Set Set.instHasSubset E	Spanning ENat instLEENat eRank eRk	—	spanning_iff_eRk_le'
spanning_iff_eRk_le' 📖	mathematical	—	Spanning ENat instLEENat eRank eRk Set Set.instHasSubset E	—	Eq.le Spanning.eRk_eq Spanning.subset_ground exists_isBasis IsBase.spanning_of_superset Indep.isBase_of_eRk_ge IsBasis.indep Indep.finite LE.le.trans IsBasis.eRk_eq_eRk IsBasis.subset

Matroid.Dep

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eRk_lt_encard 📖	mathematical	Matroid.Dep	ENat instLTENat Matroid.eRk Set.encard	—	LE.le.lt_of_ne Matroid.eRk_le_encard Matroid.indep_iff_eRk_eq_encard not_indep

Matroid.Indep

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eRk_eq_encard 📖	mathematical	Matroid.Indep	Matroid.eRk Set.encard	—	Matroid.eq_eRk_iff subset_ground isBasis_self
encard_le_eRank 📖	mathematical	Matroid.Indep	ENat instLEENat Set.encard Matroid.eRank	—	eRk_eq_encard Matroid.eRank_def Matroid.eRk_mono subset_ground
encard_le_eRk_of_subset 📖	mathematical	Matroid.Indep Set Set.instHasSubset	ENat instLEENat Set.encard Matroid.eRk	—	Matroid.eRk_mono eRk_eq_encard
exists_insert_of_encard_lt 📖	mathematical	Matroid.Indep ENat instLTENat Set.encard	Set Set.instMembership Set.instSDiff Matroid.Indep Set.instInsert	—	augment
isBase_of_eRk_ge 📖	mathematical	Matroid.Indep ENat instLEENat Matroid.eRank Matroid.eRk	Matroid.IsBase	—	isBasis_of_eRk_ge subset_ground Eq.trans_le Matroid.eRk_ground Set.instReflSubset
isBasis'_of_eRk_ge 📖	mathematical	Matroid.Indep Set Set.instHasSubset ENat instLEENat Matroid.eRk	Matroid.IsBasis'	—	Matroid.isBasis'_iff_indep_encard_eq_of_finite LE.le.antisymm Matroid.eRk_mono eRk_eq_encard
isBasis_of_eRk_ge 📖	mathematical	Matroid.Indep Set Set.instHasSubset ENat instLEENat Matroid.eRk Matroid.E	Matroid.IsBasis	—	Matroid.IsBasis'.isBasis isBasis'_of_eRk_ge

Matroid.IsBase

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eRk_eq_eRank 📖	mathematical	Matroid.IsBase	Matroid.eRk Matroid.eRank	—	Matroid.Indep.eRk_eq_encard indep Matroid.eRank_def Matroid.IsBasis.encard_eq_eRk isBasis_ground
encard_compl_eq 📖	mathematical	Matroid.IsBase	Set.encard Set Set.instSDiff Matroid.E Matroid.eRank Matroid.dual	—	encard_eq_eRank compl_isBase_dual
encard_eq_eRank 📖	mathematical	Matroid.IsBase	Set.encard Matroid.eRank	—	encard_eq_encard_of_isBase ciSup_const Matroid.instNonemptySubtypeSetIsBase

Matroid.IsBasis

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eRk_eq_eRk 📖	mathematical	Matroid.IsBasis	Matroid.eRk	—	encard_eq_eRk Matroid.Indep.eRk_eq_encard indep
eRk_eq_eRk_insert 📖	mathematical	Matroid.IsBasis	Matroid.eRk Set Set.instInsert	—	Set.union_singleton eRk_eq_eRk_union
eRk_eq_eRk_union 📖	mathematical	Matroid.IsBasis	Matroid.eRk Set Set.instUnion	—	Matroid.IsBasis'.eRk_eq_eRk_union isBasis'
eRk_eq_encard 📖	mathematical	Matroid.IsBasis	Matroid.eRk Set.encard	—	eRk_eq_eRk Matroid.Indep.eRk_eq_encard indep
encard_eq_eRk 📖	mathematical	Matroid.IsBasis	Set.encard Matroid.eRk	—	Matroid.IsBasis'.encard_eq_eRk isBasis'

Matroid.IsBasis'

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eRk_eq_eRk 📖	mathematical	Matroid.IsBasis'	Matroid.eRk	—	encard_eq_eRk Matroid.Indep.eRk_eq_encard indep
eRk_eq_eRk_insert 📖	mathematical	Matroid.IsBasis'	Matroid.eRk Set Set.instInsert	—	Set.union_singleton eRk_eq_eRk_union
eRk_eq_eRk_union 📖	mathematical	Matroid.IsBasis'	Matroid.eRk Set Set.instUnion	—	Matroid.eRk_union_closure_left_eq closure_eq_closure
eRk_eq_encard 📖	mathematical	Matroid.IsBasis'	Matroid.eRk Set.encard	—	eRk_eq_eRk Matroid.Indep.eRk_eq_encard indep
encard_eq_eRk 📖	mathematical	Matroid.IsBasis'	Set.encard Matroid.eRk	—	Matroid.IsBase.encard_eq_eRank isBase_restrict

Matroid.IsCircuit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eRk_add_one_eq 📖	mathematical	Matroid.IsCircuit	ENat instAddENat Matroid.eRk AddMonoidWithOne.toOne instAddMonoidWithOneENat Set.encard	—	Matroid.exists_isBasis subset_ground isBasis_iff_insert_eq Matroid.IsBasis.eRk_eq_encard Set.encard_insert_of_notMem

Matroid.IsLoop

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eRk_eq 📖	mathematical	Matroid.IsLoop	Matroid.eRk Set Set.instSingletonSet ENat MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat	—	Matroid.eRk_closure_eq closure Matroid.loops.eq_1 Matroid.eRk_empty

Matroid.IsNonloop

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eRk_eq 📖	mathematical	Matroid.IsNonloop	Matroid.eRk Set Set.instSingletonSet ENat AddMonoidWithOne.toOne instAddMonoidWithOneENat	—	Matroid.IsBasis.encard_eq_eRk Matroid.Indep.isBasis_self indep Set.encard_singleton

Matroid.IsRkFinite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
closure_eq_closure_of_subset_of_eRk_ge_eRk 📖	mathematical	Set Set.instHasSubset ENat instLEENat Matroid.eRk	Matroid.closure	—	Matroid.exists_isBasis' Matroid.Indep.subset_isBasis'_of_subset Matroid.IsBasis'.indep HasSubset.Subset.trans Set.instIsTransSubset Matroid.IsBasis'.subset Matroid.closure_inter_ground Matroid.IsBasis.closure_eq_closure Matroid.IsBasis'.isBasis_inter_ground Set.Finite.eq_of_subset_of_encard_le Matroid.Indep.finite_of_subset_isRkFinite Matroid.IsBasis'.eRk_eq_encard
closure_eq_closure_of_subset_of_forall_insert 📖	mathematical	Set Set.instHasSubset ENat instLEENat Matroid.eRk Set.instInsert	Matroid.closure	—	closure_eq_closure_of_subset_of_eRk_ge_eRk not_lt Matroid.exists_eRk_insert_eq_add_one_of_lt ENat.add_one_le_iff LT.lt.ne eRk_lt_top
eRk_lt_top 📖	mathematical	—	ENat instLTENat Matroid.eRk Top.top instTopENat	—	Matroid.eRk_lt_top_iff
indep_of_encard_le_eRk 📖	mathematical	ENat instLEENat Set.encard Matroid.eRk	Matroid.Indep	—	Matroid.indep_iff_eRk_eq_encard_of_finite LE.le.trans_lt eRk_lt_top LE.le.antisymm Matroid.eRk_le_encard
isBasis_of_subset_closure_of_subset_of_encard_le 📖	mathematical	Set Set.instHasSubset Matroid.closure ENat instLEENat Set.encard Matroid.eRk	Matroid.IsBasis	—	Matroid.exists_isBasis HasSubset.Subset.trans Set.instIsTransSubset Matroid.IsBasis.subset Set.inter_subset_left Matroid.closure_inter_ground Matroid.closure_subset_closure_of_subset_closure Matroid.IsBasis.subset_closure Matroid.Indep.isBasis_of_subset_of_subset_closure Matroid.IsBasis.indep Set.Finite.eq_of_subset_of_encard_le finite_of_isBasis Matroid.IsBasis.encard_eq_eRk

Matroid.Spanning

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eRank_restrict 📖	mathematical	Matroid.Spanning	Matroid.eRank Matroid.restrict	—	Matroid.eRank_def Matroid.restrict_ground_eq Matroid.restrict_eRk_eq Eq.subset Set.instReflSubset eRk_eq
eRk_eq 📖	mathematical	Matroid.Spanning	Matroid.eRk Matroid.eRank	—	Matroid.exists_isBasis subset_ground LE.le.antisymm Matroid.eRk_le_eRank Matroid.IsBasis.encard_eq_eRk Matroid.IsBase.encard_eq_eRank Matroid.IsBasis.isBase_of_spanning le_refl

---

← Back to Index