Grade

📁 Source: Mathlib/Data/Finset/Grade.lean

Statistics

Metric	Count
Definitions `instGradeMinOrder_multiset`, `instGradeMinOrder_nat`, `instGradeMinOrder`	3
Theorems `card_finset`, `card_multiset`, `exists_finset_cons`, `exists_finset_erase`, `exists_finset_insert`, `exists_multiset_cons`, `finset_coe`, `finset_val`, `coe_covBy_coe`, `coe_wcovBy_coe`, `covBy_cons`, `covBy_iff_card_sdiff_eq_one`, `covBy_iff_exists_cons`, `covBy_iff_exists_erase`, `covBy_iff_exists_insert`, `covBy_insert`, `empty_covBy_singleton`, `erase_covBy`, `erase_wcovBy`, `grade_eq`, `grade_multiset_eq`, `isAtom_iff`, `isAtom_singleton`, `isCoatom_compl_singleton`, `isCoatom_iff`, `ordConnected_range_coe`, `ordConnected_range_val`, `val_covBy_val`, `val_wcovBy_val`, `wcovBy_insert`, `covBy_cons`, `covBy_iff`, `grade_eq`, `isAtom_iff`, `isAtom_singleton`, `finset_coe`, `finset_val`	37
Total	40

CovBy

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_finset` 📖	mathematical	`CovBy` `Finset` `Preorder.toLT` `PartialOrder.toPreorder` `Finset.partialOrder`	`Finset.card`	—	`card_multiset` `Finset.val_covBy_val`
`card_multiset` 📖	mathematical	`CovBy` `Multiset` `Preorder.toLT` `PartialOrder.toPreorder` `Multiset.instPartialOrder`	`Multiset.card`	—	`exists_multiset_cons` `Multiset.card_cons` `Order.covBy_succ` `Nat.instNoMaxOrder`
`exists_finset_cons` 📖	mathematical	`CovBy` `Finset` `Preorder.toLT` `PartialOrder.toPreorder` `Finset.partialOrder`	`Finset.cons`	—	`Finset.ssubset_iff_exists_cons_subset` `lt` `HasSubset.Subset.eq_of_not_ssuperset` `Finset.instIsNonstrictStrictOrderSubsetSSubset` `Finset.instAntisymmSubset` `Finset.ssubset_cons`
`exists_finset_erase` 📖	mathematical	`CovBy` `Finset` `Preorder.toLT` `PartialOrder.toPreorder` `Finset.partialOrder`	`Finset.instMembership` `Finset.erase`	—	`Finset.coe_erase` `exists_set_sdiff_singleton` `finset_coe`
`exists_finset_insert` 📖	mathematical	`CovBy` `Finset` `Preorder.toLT` `PartialOrder.toPreorder` `Finset.partialOrder`	`Finset.instMembership` `Finset.instInsert`	—	`Finset.cons_eq_insert` `exists_finset_cons`
`exists_multiset_cons` 📖	mathematical	`CovBy` `Multiset` `Preorder.toLT` `PartialOrder.toPreorder` `Multiset.instPartialOrder`	`Multiset.cons`	—	`LE.le.eq_of_not_lt` `Multiset.lt_cons_self` `Multiset.lt_iff_cons_le` `lt`
`finset_coe` 📖	mathematical	`CovBy` `Finset` `Preorder.toLT` `PartialOrder.toPreorder` `Finset.partialOrder`	`Set` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `SetLike.coe` `Finset.instSetLike`	—	`Finset.coe_covBy_coe`
`finset_val` 📖	mathematical	`CovBy` `Finset` `Preorder.toLT` `PartialOrder.toPreorder` `Finset.partialOrder`	`Multiset` `Multiset.instPartialOrder` `Finset.val`	—	`Finset.val_covBy_val`

Finset

Definitions

Name	Category	Theorems
`instGradeMinOrder_multiset` 📖	CompOp	1 math math: `grade_multiset_eq`
`instGradeMinOrder_nat` 📖	CompOp	1 math math: `grade_eq`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_covBy_coe` 📖	mathematical	—	`CovBy` `Set` `Preorder.toLT` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `SetLike.coe` `Finset` `instSetLike` `partialOrder`	—	`Set.OrdConnected.apply_covBy_apply_iff` `coe_injective` `coe_subset` `ordConnected_range_coe`
`coe_wcovBy_coe` 📖	mathematical	—	`WCovBy` `Set` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `SetLike.coe` `Finset` `instSetLike` `partialOrder`	—	`Set.OrdConnected.apply_wcovBy_apply_iff` `coe_injective` `coe_subset` `ordConnected_range_coe`
`covBy_cons` 📖	mathematical	`Finset` `instMembership`	`CovBy` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `cons`	—	—
`covBy_iff_card_sdiff_eq_one` 📖	mathematical	—	`CovBy` `Finset` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `instHasSubset` `card` `instSDiff`	—	`covBy_iff_exists_insert` `insert_sdiff_cancel` `card_singleton` `mem_sdiff` `superset_of_eq` `instReflSubset` `mem_singleton_self` `insert_eq` `sdiff_union_of_subset`
`covBy_iff_exists_cons` 📖	mathematical	—	`CovBy` `Finset` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `cons`	—	`CovBy.exists_finset_cons` `covBy_cons`
`covBy_iff_exists_erase` 📖	mathematical	—	`CovBy` `Finset` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `instMembership` `erase`	—	`coe_erase`
`covBy_iff_exists_insert` 📖	mathematical	—	`CovBy` `Finset` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `instMembership` `instInsert`	—	`coe_insert`
`covBy_insert` 📖	mathematical	`Finset` `instMembership`	`CovBy` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `instInsert`	—	`WCovBy.covBy_of_lt` `wcovBy_insert` `ssubset_insert`
`empty_covBy_singleton` 📖	mathematical	—	`CovBy` `Finset` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `instEmptyCollection` `instSingleton`	—	`covBy_insert` `instLawfulSingleton` `notMem_empty`
`erase_covBy` 📖	mathematical	`Finset` `instMembership`	`CovBy` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `erase`	—	`erase_ssubset` `erase_wcovBy`
`erase_wcovBy` 📖	mathematical	—	`WCovBy` `Finset` `PartialOrder.toPreorder` `partialOrder` `erase`	—	`coe_erase`
`grade_eq` 📖	mathematical	—	`grade` `Finset` `Nat.instPreorder` `PartialOrder.toPreorder` `partialOrder` `GradeMinOrder.toGradeOrder` `instGradeMinOrder_nat` `card`	—	—
`grade_multiset_eq` 📖	mathematical	—	`grade` `Multiset` `Finset` `PartialOrder.toPreorder` `Multiset.instPartialOrder` `partialOrder` `GradeMinOrder.toGradeOrder` `instGradeMinOrder_multiset` `val`	—	—
`isAtom_iff` 📖	mathematical	—	`IsAtom` `Finset` `PartialOrder.toPreorder` `partialOrder` `instOrderBot` `instSingleton`	—	—
`isAtom_singleton` 📖	mathematical	—	`IsAtom` `Finset` `PartialOrder.toPreorder` `partialOrder` `instOrderBot` `instSingleton`	—	`singleton_ne_empty` `eq_empty_of_ssubset_singleton`
`isCoatom_compl_singleton` 📖	mathematical	—	`IsCoatom` `Finset` `PartialOrder.toPreorder` `partialOrder` `CoheytingAlgebra.toOrderTop` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `booleanAlgebra` `Compl.compl` `BooleanAlgebra.toCompl` `instSingleton`	—	`IsAtom.compl` `isAtom_singleton`
`isCoatom_iff` 📖	mathematical	—	`IsCoatom` `Finset` `PartialOrder.toPreorder` `partialOrder` `CoheytingAlgebra.toOrderTop` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `booleanAlgebra` `Compl.compl` `BooleanAlgebra.toCompl` `instSingleton`	—	—
`ordConnected_range_coe` 📖	mathematical	—	`Set.OrdConnected` `Set` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `Set.range` `Finset` `SetLike.coe` `instSetLike`	—	`Set.Finite.subset` `finite_toSet` `Set.Finite.coe_toFinset`
`ordConnected_range_val` 📖	mathematical	—	`Set.OrdConnected` `Multiset` `PartialOrder.toPreorder` `Multiset.instPartialOrder` `Set.range` `Finset` `val`	—	`Multiset.nodup_of_le` `nodup`
`val_covBy_val` 📖	mathematical	—	`CovBy` `Multiset` `Preorder.toLT` `PartialOrder.toPreorder` `Multiset.instPartialOrder` `val` `Finset` `partialOrder`	—	`Set.OrdConnected.apply_covBy_apply_iff` `val_injective` `val_le_iff` `ordConnected_range_val`
`val_wcovBy_val` 📖	mathematical	—	`WCovBy` `Multiset` `PartialOrder.toPreorder` `Multiset.instPartialOrder` `val` `Finset` `partialOrder`	—	`Set.OrdConnected.apply_wcovBy_apply_iff` `val_injective` `val_le_iff` `ordConnected_range_val`
`wcovBy_insert` 📖	mathematical	—	`WCovBy` `Finset` `PartialOrder.toPreorder` `partialOrder` `instInsert`	—	`coe_insert`

Multiset

Definitions

Name	Category	Theorems
`instGradeMinOrder` 📖	CompOp	1 math math: `grade_eq`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`covBy_cons` 📖	mathematical	—	`CovBy` `Multiset` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrder` `cons`	—	`lt_cons_self` `Order.covBy_succ` `Nat.instNoMaxOrder` `card_lt_card` `card_cons`
`covBy_iff` 📖	mathematical	—	`CovBy` `Multiset` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrder` `cons`	—	`CovBy.exists_multiset_cons` `covBy_cons`
`grade_eq` 📖	mathematical	—	`grade` `Multiset` `Nat.instPreorder` `PartialOrder.toPreorder` `instPartialOrder` `GradeMinOrder.toGradeOrder` `instGradeMinOrder` `card`	—	—
`isAtom_iff` 📖	mathematical	—	`IsAtom` `Multiset` `PartialOrder.toPreorder` `instPartialOrder` `instOrderBot` `instSingleton`	—	—
`isAtom_singleton` 📖	mathematical	—	`IsAtom` `Multiset` `PartialOrder.toPreorder` `instPartialOrder` `instOrderBot` `instSingleton`	—	`isAtom_iff`

WCovBy

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finset_coe` 📖	mathematical	`WCovBy` `Finset` `PartialOrder.toPreorder` `Finset.partialOrder`	`Set` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `SetLike.coe` `Finset.instSetLike`	—	`Finset.coe_wcovBy_coe`
`finset_val` 📖	mathematical	`WCovBy` `Finset` `PartialOrder.toPreorder` `Finset.partialOrder`	`Multiset` `Multiset.instPartialOrder` `Finset.val`	—	`Finset.val_wcovBy_val`

---

← Back to Index