Cardinal

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

Statistics

Metric	Count
Definitions InvariantCardinalRank, cRank, cRk	3
Theorems cRk_eq_cardinalMk, cardinalMk_le_cRank, cardinalMk_le_cRk_of_subset, cardinalMk_le_isBase, cardinalMk_le_isBasis, cardinalMk_le_isBasis', isBase_of_cRank_le, isBase_of_cRank_le_of_finite, forall_card_isBasis_diff, cardinalMk_diff_comm, cardinalMk_eq, cardinalMk_eq_cRank, cardinalMk_le_cRank, cardinalMk_diff_comm, cardinalMk_eq, cardinalMk_eq_cRk, cardinalMk_le_cRk, cardinalMk_diff_comm, cardinalMk_eq, cardinalMk_eq_cRk, cardinalMk_le_cRk, cRank_le_cardinalMk, isBase_of_le_cRank, isBase_of_le_cRank_of_finite, cRank_eq_iSup_cardinalMk_indep, cRank_le_iff, cRank_restrict, cRk_closure, cRk_closure_congr, cRk_comap, cRk_comap_lift, cRk_ground, cRk_insert_closure_eq, cRk_inter_add_cRk_union_le, cRk_inter_ground, cRk_le_cardinalMk, cRk_le_iff, cRk_le_of_subset, cRk_map_eq, cRk_map_image, cRk_map_image_lift, cRk_mono, cRk_restrict, cRk_restrict_subset, cRk_union_closure_eq, cRk_union_closure_left_eq, cRk_union_closure_right_eq, invariantCardinalRank_comap, invariantCardinalRank_iff, invariantCardinalRank_map, invariantCardinalRank_of_finitary, invariantCardinalRank_restrict, isRkFinite_iff_cRk_lt_aleph0, rankFinite_iff_cRank_lt_aleph0, rankInfinite_iff_aleph0_le_cRank, toENat_cRank_eq, toENat_cRk_eq	57
Total	60

Matroid

Definitions

Name	Category	Theorems
InvariantCardinalRank 📖	CompData	5 math math: invariantCardinalRank_map, invariantCardinalRank_comap, invariantCardinalRank_of_finitary, invariantCardinalRank_iff, invariantCardinalRank_restrict
cRank 📖	CompOp	12 math math: IsBase.cardinalMk_le_cRank, cRank_eq_iSup_cardinalMk_indep, cRk_ground, AlgebraicIndependent.matroid_cRank_eq, IsBase.cardinalMk_eq_cRank, cRank_le_iff, Indep.cardinalMk_le_cRank, rankInfinite_iff_aleph0_le_cRank, cRank_restrict, rankFinite_iff_cRank_lt_aleph0, Spanning.cRank_le_cardinalMk, toENat_cRank_eq
cRk 📖	CompOp	29 math math: cRk_union_closure_left_eq, Indep.cardinalMk_le_cRk_of_subset, cRk_comap_lift, isRkFinite_iff_cRk_lt_aleph0, cRk_restrict_subset, cRk_inter_ground, cRk_ground, cRk_le_cardinalMk, cRk_closure, cRk_mono, IsBasis.cardinalMk_le_cRk, cRk_map_eq, IsBasis'.cardinalMk_eq_cRk, cRk_union_closure_eq, cRk_insert_closure_eq, cRk_map_image, cRk_le_iff, cRank_restrict, cRk_inter_add_cRk_union_le, cRk_map_image_lift, cRk_comap, IsBasis.cardinalMk_eq_cRk, cRk_closure_congr, Indep.cRk_eq_cardinalMk, cRk_le_of_subset, cRk_union_closure_right_eq, IsBasis'.cardinalMk_le_cRk, toENat_cRk_eq, cRk_restrict

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cRank_eq_iSup_cardinalMk_indep 📖	mathematical	—	cRank iSup Cardinal Set Indep ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder Cardinal.instConditionallyCompleteLinearOrderBot Set.Elem	—	LE.le.antisymm ciSup_le' le_ciSup_of_le Cardinal.bddAbove_range small_subtype small_set UnivLE.small UnivLE.self IsBase.indep le_refl Indep.exists_isBase_superset Cardinal.mk_le_mk_of_subset
cRank_le_iff 📖	mathematical	—	Cardinal Cardinal.instLE cRank Set.Elem	—	LE.le.trans IsBase.cardinalMk_le_cRank ciSup_le instNonemptySubtypeSetIsBase
cRank_restrict 📖	mathematical	—	cRank restrict cRk	—	—
cRk_closure 📖	mathematical	—	cRk closure	—	exists_isBasis' IsBasis.cardinalMk_eq_cRk IsBasis'.isBasis_closure_right IsBasis'.cardinalMk_eq_cRk
cRk_closure_congr 📖	mathematical	closure	cRk	—	cRk_closure
cRk_comap 📖	mathematical	—	cRk comap Set.image	—	cRk_comap_lift
cRk_comap_lift 📖	mathematical	—	Cardinal.lift cRk comap Set.image	—	cRk.eq_1 cRank.eq_1 le_antisymm_iff Cardinal.lift_iSup Cardinal.bddAbove_range small_subtype small_set UnivLE.small UnivLE.self ciSup_le_iff instNonemptySubtypeSetIsBase univLE_of_max Cardinal.mk_image_eq_of_injOn_lift Cardinal.lift_le IsBasis'.cardinalMk_le_cRk Set.exists_subset_bijOn HasSubset.Subset.trans Set.instIsTransSubset Set.inter_subset_right Set.BijOn.image_eq Set.image_preimage_inter Set.inter_eq_self_of_subset_left IsBasis'.subset Set.BijOn.injOn comap_isBasis'_iff
cRk_ground 📖	mathematical	—	cRk E cRank	—	cRk.eq_1 restrict_ground_eq_self
cRk_insert_closure_eq 📖	mathematical	—	cRk Set Set.instInsert closure	—	Set.union_singleton cRk_union_closure_left_eq
cRk_inter_add_cRk_union_le 📖	mathematical	—	Cardinal Cardinal.instLE Cardinal.instAdd cRk 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 cRk_union_closure_eq IsBasis'.closure_eq_closure IsBasis'.cardinalMk_eq_cRk Cardinal.mk_union_add_mk_inter add_comm add_le_add Cardinal.addLeftMono Cardinal.addRightMono cRk_le_cardinalMk Cardinal.mk_le_mk_of_subset Set.subset_inter
cRk_inter_ground 📖	mathematical	—	cRk Set Set.instInter E	—	LE.le.antisymm cRk_le_of_subset Set.inter_subset_left cRk_le_iff IsBasis.cardinalMk_le_cRk IsBasis'.isBasis_inter_ground
cRk_le_cardinalMk 📖	mathematical	—	Cardinal Cardinal.instLE cRk Set.Elem	—	ciSup_le instNonemptySubtypeSetIsBase Cardinal.mk_le_mk_of_subset IsBase.subset_ground
cRk_le_iff 📖	mathematical	—	Cardinal Cardinal.instLE cRk Set.Elem	—	—
cRk_le_of_subset 📖	mathematical	Set Set.instHasSubset	Cardinal Cardinal.instLE cRk	—	cRk_mono
cRk_map_eq 📖	mathematical	Set.InjOn E	cRk map Set.preimage	—	cRk_inter_ground cRk_map_image Set.image_preimage_inter map_ground
cRk_map_image 📖	mathematical	Set.InjOn E Set Set.instHasSubset	cRk map Set.image	—	cRk_map_image_lift
cRk_map_image_lift 📖	mathematical	Set.InjOn E Set Set.instHasSubset	Cardinal.lift cRk map Set.image	—	cRk.eq_1 cRank.eq_1 le_antisymm_iff Cardinal.lift_iSup Cardinal.bddAbove_range small_subtype small_set UnivLE.small UnivLE.self ciSup_le_iff instNonemptySubtypeSetIsBase univLE_of_max isBasis'_iff_isBasis Set.image_mono map_isBasis_iff' Cardinal.mk_image_eq_of_injOn_lift Set.InjOn.mono Indep.subset_ground IsBasis.indep Cardinal.lift_le IsBasis.cardinalMk_le_cRk Set.InjOn.image_eq_image_iff IsBasis.subset_ground IsBasis.map
cRk_mono 📖	mathematical	—	Monotone Set Cardinal PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Cardinal.partialOrder cRk	—	Indep.subset_isBasis'_of_subset IsBasis'.indep HasSubset.Subset.trans Set.instIsTransSubset IsBasis'.subset LE.le.trans Cardinal.mk_le_mk_of_subset IsBasis'.cardinalMk_le_cRk
cRk_restrict 📖	mathematical	—	cRk restrict Set Set.instInter	—	cRk_inter_ground restrict_ground_eq cRk_restrict_subset Set.inter_subset_right Set.inter_comm
cRk_restrict_subset 📖	mathematical	Set Set.instHasSubset	cRk restrict	—	Set.inter_eq_self_of_subset_left HasSubset.Subset.trans Set.instIsTransSubset IsBasis'.subset IsBasis'.cardinalMk_le_cRk
cRk_union_closure_eq 📖	mathematical	—	cRk Set Set.instUnion closure	—	cRk_union_closure_right_eq cRk_union_closure_left_eq
cRk_union_closure_left_eq 📖	mathematical	—	cRk Set Set.instUnion closure	—	cRk_closure_congr closure_union_closure_left_eq
cRk_union_closure_right_eq 📖	mathematical	—	cRk Set Set.instUnion closure	—	cRk_closure_congr closure_union_closure_right_eq
invariantCardinalRank_comap 📖	mathematical	—	InvariantCardinalRank comap	—	comap_isBasis_iff Cardinal.mk_image_eq_of_injOn_lift Set.InjOn.mono Set.diff_subset Set.InjOn.image_diff Set.diff_union_diff_cancel Set.inter_subset_left Set.image_inter_subset Set.inter_comm Set.diff_inter_self_eq_diff Cardinal.mk_union_of_disjoint Disjoint.mono_right HasSubset.Subset.trans Set.instIsTransSubset Set.disjoint_sdiff_left IsBasis.cardinalMk_diff_comm
invariantCardinalRank_iff 📖	mathematical	—	InvariantCardinalRank Set.Elem Set Set.instSDiff	—	—
invariantCardinalRank_map 📖	mathematical	Set.InjOn E	InvariantCardinalRank map	—	map_isBasis_iff' IsBasis.cardinalMk_diff_comm Set.diff_self_inter Set.diff_inter_self_eq_diff Set.InjOn.image_inter Indep.subset_ground IsBasis.indep Set.inter_comm Set.InjOn.image_diff Set.InjOn.mono Cardinal.mk_image_eq_of_injOn_lift Indep.diff Set.InjOn.image_eq_image_iff IsBasis.subset_ground
invariantCardinalRank_of_finitary 📖	mathematical	—	InvariantCardinalRank	—	Set.cast_ncard IsBase.diff_finite_comm IsBase.ncard_diff_comm le_refl IsBase.insert_dep IsBase.subset_ground Mathlib.Tactic.Contrapose.contrapose₂ Mathlib.Tactic.Push.not_and_eq Finitary.indep_of_forall_finite Indep.subset Set.Finite.to_subtype Set.Finite.diff Set.diff_singleton_subset_iff Set.subset_insert_diff_singleton Set.diff_inter_self_eq_diff Set.diff_subset_iff Set.inter_comm Set.union_subset Set.inter_subset_left Set.iUnion_subset IsBase.exists_insert_of_ssubset Set.insert_subset_insert HasSubset.Subset.trans Set.instIsTransSubset Set.subset_iUnion_of_subset subset_rfl Set.instReflSubset Set.subset_union_right LE.le.trans Cardinal.mk_le_mk_of_subset Cardinal.mk_iUnion_le Cardinal.mul_le_max_of_aleph0_le_left Set.infinite_coe_iff Set.Infinite.eq_1 ciSup_le' LT.lt.le Cardinal.lt_aleph0_of_finite LE.le.antisymm restrict_finitary IsBasis.isBase_restrict
invariantCardinalRank_restrict 📖	mathematical	—	InvariantCardinalRank restrict	—	IsBasis.cardinalMk_diff_comm isBasis_restrict_iff'
isRkFinite_iff_cRk_lt_aleph0 📖	mathematical	—	IsRkFinite Cardinal Preorder.toLT PartialOrder.toPreorder Cardinal.partialOrder cRk Cardinal.aleph0	—	IsRkFinite.eq_1 rankFinite_iff_cRank_lt_aleph0 cRank_restrict
rankFinite_iff_cRank_lt_aleph0 📖	mathematical	—	RankFinite Cardinal Preorder.toLT PartialOrder.toPreorder Cardinal.partialOrder cRank Cardinal.aleph0	—	Cardinal.lt_aleph0_iff_finite IsBase.cardinalMk_eq_cRank invariantCardinalRank_of_finitary finitary_of_rankFinite exists_isBase LE.le.trans_lt IsBase.cardinalMk_le_cRank
rankInfinite_iff_aleph0_le_cRank 📖	mathematical	—	RankInfinite Cardinal Cardinal.instLE Cardinal.aleph0 cRank	—	not_lt rankFinite_iff_cRank_lt_aleph0 not_rankFinite_iff
toENat_cRank_eq 📖	mathematical	—	DFunLike.coe OrderRingHom Cardinal ENat Semiring.toNonAssocSemiring CommSemiring.toSemiring Cardinal.commSemiring PartialOrder.toPreorder Cardinal.partialOrder instCommSemiringENat SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderENat OrderRingHom.instFunLike Cardinal.toENat cRank eRank	—	rankFinite_or_rankInfinite exists_isBase IsBase.cardinalMk_eq_cRank invariantCardinalRank_of_finitary finitary_of_rankFinite IsBase.encard_eq_eRank Set.toENat_cardinalMk eRank_eq_top rankInfinite_iff_aleph0_le_cRank
toENat_cRk_eq 📖	mathematical	—	DFunLike.coe OrderRingHom Cardinal ENat Semiring.toNonAssocSemiring CommSemiring.toSemiring Cardinal.commSemiring PartialOrder.toPreorder Cardinal.partialOrder instCommSemiringENat SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderENat OrderRingHom.instFunLike Cardinal.toENat cRk eRk	—	cRk.eq_1 toENat_cRank_eq eRk.eq_1

Matroid.Indep

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cRk_eq_cardinalMk 📖	mathematical	Matroid.Indep	Set.Elem Matroid.cRk	—	LE.le.antisymm' Matroid.cRk_le_cardinalMk Matroid.IsBasis.cardinalMk_le_cRk isBasis_self
cardinalMk_le_cRank 📖	mathematical	Matroid.Indep	Cardinal Cardinal.instLE Set.Elem Matroid.cRank	—	exists_isBase_superset le_ciSup_of_le Cardinal.bddAbove_range small_subtype small_set UnivLE.small UnivLE.self Cardinal.mk_le_mk_of_subset
cardinalMk_le_cRk_of_subset 📖	mathematical	Matroid.Indep Set Set.instHasSubset	Cardinal Cardinal.instLE Set.Elem Matroid.cRk	—	subset_isBasis'_of_subset LE.le.trans Cardinal.mk_le_mk_of_subset Matroid.IsBasis'.cardinalMk_le_cRk
cardinalMk_le_isBase 📖	mathematical	Matroid.Indep Matroid.IsBase	Cardinal Cardinal.instLE Set.Elem	—	exists_isBase_superset Cardinal.mk_le_mk_of_subset Matroid.IsBase.cardinalMk_eq
cardinalMk_le_isBasis 📖	mathematical	Matroid.Indep Matroid.IsBasis Set Set.instHasSubset	Cardinal Cardinal.instLE Set.Elem	—	cardinalMk_le_isBasis' Matroid.IsBasis.isBasis'
cardinalMk_le_isBasis' 📖	mathematical	Matroid.Indep Matroid.IsBasis' Set Set.instHasSubset	Cardinal Cardinal.instLE Set.Elem	—	subset_isBasis'_of_subset Cardinal.mk_le_mk_of_subset Matroid.IsBasis'.cardinalMk_eq
isBase_of_cRank_le 📖	mathematical	Matroid.Indep Cardinal Cardinal.instLE Matroid.cRank Set.Elem	Matroid.IsBase	—	isBase_of_maximal Set.Finite.eq_of_subset_of_encard_le finite OrderRingHom.monotone' LE.le.trans cardinalMk_le_cRank
isBase_of_cRank_le_of_finite 📖	mathematical	Matroid.Indep Cardinal Cardinal.instLE Matroid.cRank Set.Elem	Matroid.IsBase	—	Matroid.rankFinite_iff_cRank_lt_aleph0 LE.le.trans_lt Cardinal.lt_aleph0_iff_finite isBase_of_cRank_le

Matroid.InvariantCardinalRank

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
forall_card_isBasis_diff 📖	mathematical	Matroid.IsBasis	Set.Elem Set Set.instSDiff	—	—

Matroid.IsBase

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cardinalMk_diff_comm 📖	mathematical	Matroid.IsBase	Set.Elem Set Set.instSDiff	—	Matroid.IsBasis.cardinalMk_diff_comm isBasis_ground
cardinalMk_eq 📖	mathematical	Matroid.IsBase	Set.Elem	—	Matroid.IsBasis.cardinalMk_eq isBasis_ground
cardinalMk_eq_cRank 📖	mathematical	Matroid.IsBase	Set.Elem Matroid.cRank	—	cardinalMk_eq ciSup_const Matroid.instNonemptySubtypeSetIsBase
cardinalMk_le_cRank 📖	mathematical	Matroid.IsBase	Cardinal Cardinal.instLE Set.Elem Matroid.cRank	—	le_ciSup Cardinal.bddAbove_range small_subtype small_set UnivLE.small UnivLE.self

Matroid.IsBasis

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cardinalMk_diff_comm 📖	mathematical	Matroid.IsBasis	Set.Elem Set Set.instSDiff	—	Matroid.InvariantCardinalRank.forall_card_isBasis_diff
cardinalMk_eq 📖	mathematical	Matroid.IsBasis	Set.Elem	—	Set.diff_union_inter Cardinal.mk_union_of_disjoint Disjoint.mono_right Set.inter_subset_right Set.disjoint_sdiff_left cardinalMk_diff_comm Set.inter_subset_left Set.inter_comm
cardinalMk_eq_cRk 📖	mathematical	Matroid.IsBasis	Set.Elem Matroid.cRk	—	Matroid.IsBasis'.cardinalMk_eq_cRk isBasis'
cardinalMk_le_cRk 📖	mathematical	Matroid.IsBasis	Cardinal Cardinal.instLE Set.Elem Matroid.cRk	—	Matroid.IsBasis'.cardinalMk_le_cRk isBasis'

Matroid.IsBasis'

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cardinalMk_diff_comm 📖	mathematical	Matroid.IsBasis'	Set.Elem Set Set.instSDiff	—	Matroid.IsBasis.cardinalMk_diff_comm isBasis_inter_ground
cardinalMk_eq 📖	mathematical	Matroid.IsBasis'	Set.Elem	—	Matroid.IsBasis.cardinalMk_eq isBasis_inter_ground
cardinalMk_eq_cRk 📖	mathematical	Matroid.IsBasis'	Set.Elem Matroid.cRk	—	Matroid.cRk.eq_1 Matroid.IsBase.cardinalMk_eq_cRank Matroid.invariantCardinalRank_restrict Matroid.isBase_restrict_iff'
cardinalMk_le_cRk 📖	mathematical	Matroid.IsBasis'	Cardinal Cardinal.instLE Set.Elem Matroid.cRk	—	Matroid.IsBase.cardinalMk_le_cRank Matroid.isBase_restrict_iff'

Matroid.Spanning

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cRank_le_cardinalMk 📖	mathematical	Matroid.Spanning	Cardinal Cardinal.instLE Matroid.cRank Set.Elem	—	exists_isBase_subset Eq.trans_le Matroid.IsBase.cardinalMk_eq_cRank Cardinal.mk_le_mk_of_subset
isBase_of_le_cRank 📖	mathematical	Matroid.Spanning Cardinal Cardinal.instLE Set.Elem Matroid.cRank	Matroid.IsBase	—	exists_isBase_subset Set.Finite.eq_of_subset_of_encard_le Matroid.IsBase.finite OrderRingHom.monotone' LE.le.trans Eq.ge Matroid.IsBase.cardinalMk_eq_cRank Matroid.invariantCardinalRank_of_finitary Matroid.finitary_of_rankFinite
isBase_of_le_cRank_of_finite 📖	mathematical	Matroid.Spanning Cardinal Cardinal.instLE Set.Elem Matroid.cRank	Matroid.IsBase	—	exists_isBase_subset Matroid.IsBase.rankFinite_of_finite Set.Finite.subset isBase_of_le_cRank

---

← Back to Index