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	82 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_compl_insert_union_add_eRk_compl_insert_inter_le`, `IsBasis'.encard_eq_eRk`, `eRk_insert_le_add_one`, `spanning_iff_eRk_le'`, `IsBasis.eRk_eq_eRk_insert`, `eRk_union_ground`, `eRk_inter_add_eRk_union_le`, `IsBasis.encard_eq_eRk`, `eRk_dual_add_eRank`, `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_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` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `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` `instZeroENat`	—	`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` `instZeroENat` `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` `Preorder.toLE` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `eRank` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `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` `Preorder.toLE` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `eRank` `Set.encard` `E`	—	`Eq.trans_le` `eRank_def` `eRk_le_encard`
`eRank_loopyOn` 📖	mathematical	—	`eRank` `loopyOn` `ENat` `instZeroENat`	—	`eRank_def` `eRk_loopyOn`
`eRank_lt_top_iff` 📖	mathematical	—	`ENat` `Preorder.toLT` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `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` `Preorder.toLE` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `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` `Preorder.toLE` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `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.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` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `eRk` `dual` `eRank` `Set.instSDiff` `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` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `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` `instZeroENat`	—	`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` `Preorder.toLE` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `eRk` `instZeroENat`	`Set` `Set.instSDiff`	—	`eRk_eq_eRk_union_eRk_le_zero` `Set.diff_union_self`
`eRk_eq_eRk_of_subset_of_le` 📖	—	`Set` `Set.instHasSubset` `ENat` `Preorder.toLE` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `eRk`	—	—	`LE.le.antisymm` `eRk_mono`
`eRk_eq_eRk_union_eRk_le_zero` 📖	mathematical	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `eRk` `instZeroENat`	`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` 📖	—	`Set` `Set.instHasSubset` `ENat` `Preorder.toLE` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `eRk` `Set.instInsert`	—	—	`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` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `Set.instMembership` `IsNonloop` `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` `instZeroENat` `loops`	—	`eRk_eq_zero_iff'` `Set.inter_eq_self_of_subset_left`
`eRk_eq_zero_iff'` 📖	mathematical	—	`eRk` `ENat` `instZeroENat` `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.instInsert` `ENat` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`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` `Preorder.toLE` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `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` `Preorder.toLE` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `eRk` `Set` `Set.instInsert` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`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.instInsert`	—	`eRk_inter_ground` `Set.insert_inter_of_notMem`
`eRk_inter_add_eRk_union_le` 📖	mathematical	—	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `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` `Preorder.toLE` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `eRk` `eRank`	—	`eRank_def` `eRk_inter_ground` `eRk_mono` `Set.inter_subset_right`
`eRk_le_eRk_add_eRk_diff` 📖	mathematical	`Set` `Set.instHasSubset`	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `eRk` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `Set.instSDiff`	—	`Set.union_diff_cancel` `eRk_union_le_eRk_add_eRk`
`eRk_le_eRk_inter_add_eRk_diff` 📖	mathematical	—	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `eRk` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `Set` `Set.instInter` `Set.instSDiff`	—	`Set.inter_union_diff` `eRk_union_le_eRk_add_eRk`
`eRk_le_encard` 📖	mathematical	—	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `eRk` `Set.encard`	—	`exists_isBasis'` `IsBasis'.eRk_eq_encard` `Set.encard_mono` `IsBasis'.subset`
`eRk_le_iff` 📖	mathematical	—	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `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` `Preorder.toLE` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `eRk` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `Set.instMembership` `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` `instZeroENat`	—	—
`eRk_loopyOn` 📖	mathematical	—	`eRk` `loopyOn` `ENat` `instZeroENat`	—	`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` `Preorder.toLT` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `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` `Preorder.toLT` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `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` `Preorder.toLT` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `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` `Preorder.toLT` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `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` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `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.instSingletonSet` `ENat` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat`	—	`IsNonloop.eRk_eq` `isNonloop_of_loopless`
`eRk_singleton_eq_one_iff` 📖	mathematical	—	`eRk` `Set` `Set.instSingletonSet` `ENat` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `IsNonloop`	—	`indep_singleton` `indep_iff_eRk_eq_encard_of_finite` `Set.encard_singleton` `IsNonloop.eRk_eq`
`eRk_singleton_le` 📖	mathematical	—	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `eRk` `Set` `Set.instSingletonSet` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat`	—	`LE.le.trans_eq` `eRk_le_encard` `Set.encard_singleton`
`eRk_submod` 📖	mathematical	—	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `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` `Preorder.toLE` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `eRk` `Set` `Set.instUnion` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat`	—	`LE.le.trans` `le_add_self` `eRk_submod`
`eRk_union_le_eRk_add_encard` 📖	mathematical	—	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `eRk` `Set` `Set.instUnion` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `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` `Preorder.toLE` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `eRk` `Set` `Set.instUnion` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `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` `IsBasis` `Set.encard`	—	`exists_isBasis` `IsBasis.encard_eq_eRk`
`eq_loopyOn_iff_eRank` 📖	mathematical	—	`loopyOn` `eRank` `ENat` `instZeroENat` `E`	—	`eRank_loopyOn` `eRank_eq_zero_iff`
`exists_eRk_insert_eq_add_one_of_lt` 📖	mathematical	`ENat` `Preorder.toLT` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `eRk`	`Set` `Set.instMembership` `Set.instSDiff` `Set.instInsert` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`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` `instZeroENat`	`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` `Indep` `Set.encard` `eRk`	—	`isBasis'_iff_isBasis` `isBasis'_iff_indep_encard_eq_of_finite`
`le_eRk_iff` 📖	mathematical	—	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `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` `Preorder.toLE` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `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` `Preorder.toLE` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `eRank` `eRk`	—	`spanning_iff_eRk_le'`
`spanning_iff_eRk_le'` 📖	mathematical	—	`Spanning` `ENat` `Preorder.toLE` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `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` `Preorder.toLT` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `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` `Preorder.toLE` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `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` `Preorder.toLE` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `Set.encard` `Matroid.eRk`	—	`Matroid.eRk_mono` `eRk_eq_encard`
`exists_insert_of_encard_lt` 📖	mathematical	`Matroid.Indep` `ENat` `Preorder.toLT` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `Set.encard`	`Set` `Set.instMembership` `Set.instSDiff` `Set.instInsert`	—	`augment`
`isBase_of_eRk_ge` 📖	mathematical	`Matroid.Indep` `ENat` `Preorder.toLE` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `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` `Preorder.toLE` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `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` `Preorder.toLE` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `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` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `Matroid.eRk` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `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` `instZeroENat`	—	`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` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat`	—	`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` `Preorder.toLE` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `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` `Preorder.toLE` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `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` `Preorder.toLT` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `Matroid.eRk` `Top.top` `instTopENat`	—	`Matroid.eRk_lt_top_iff`
`indep_of_encard_le_eRk` 📖	mathematical	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `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` `Preorder.toLE` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `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