Documentation Verification Report

Finite

📁 Source: Mathlib/Order/Atoms/Finite.lean

Statistics

Metric	Count
Definitions `instFintypeOfDecidableEq`	1
Theorems `instIsSimpleOrder`, `to_isAtomic`, `to_isCoatomic`, `card`, `univ`, `instFinite`, `exists_covby_infinite_Ici_of_infinite_Ici`, `exists_covby_infinite_Iic_of_infinite_Iic`, `instIsStronglyAtomic`, `instIsStronglyCoatomic`	10
Total	11

Bool

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsSimpleOrder` 📖	mathematical	—	`IsSimpleOrder` `instBoundedOrder`	—	`instNontrivial` `Finset.mem_singleton` `Finset.mem_insert` `top_eq_true` `bot_eq_false` `Fintype.univ_bool` `Finset.mem_univ`

Finite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`to_isAtomic` 📖	mathematical	—	`IsAtomic`	—	`isCoatomic_dual_iff_isAtomic` `to_isCoatomic` `OrderDual.finite`
`to_isCoatomic` 📖	mathematical	—	`IsCoatomic`	—	`IsStronglyCoatomic.toIsCoatomic` `instIsStronglyCoatomicOfWellFoundedGT` `to_wellFoundedGT`

Fintype.IsSimpleOrder

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card` 📖	mathematical	—	`Fintype.card` `IsSimpleOrder.instFintypeOfDecidableEq`	—	`Fintype.ofEquiv_card` `Fintype.card_bool`
`univ` 📖	mathematical	—	`Finset.univ` `IsSimpleOrder.instFintypeOfDecidableEq` `Finset` `Finset.instInsert` `Top.top` `OrderTop.toTop` `BoundedOrder.toOrderTop` `Finset.instSingleton` `Bot.bot` `OrderBot.toBot` `BoundedOrder.toOrderBot`	—	`Finset.ext` `IsSimpleOrder.eq_bot_or_eq_top`

IsSimpleOrder

Definitions

Name	Category	Theorems
`instFintypeOfDecidableEq` 📖	CompOp	2 math math: `Fintype.IsSimpleOrder.univ`, `Fintype.IsSimpleOrder.card`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instFinite` 📖	mathematical	—	`Finite`	—	`Finite.of_fintype`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_covby_infinite_Ici_of_infinite_Ici` 📖	mathematical	`Set.Infinite` `Set.Ici` `PartialOrder.toPreorder`	`CovBy` `Preorder.toLT`	—	`Set.Finite.not_infinite` `Set.Finite.subset` `Set.Finite.biUnion` `Mathlib.Tactic.Push.not_and_eq` `LT.lt.exists_covby_le` `LE.le.lt_of_ne` `Set.mem_biUnion` `Set.Infinite.diff` `Set.finite_singleton`
`exists_covby_infinite_Iic_of_infinite_Iic` 📖	mathematical	`Set.Infinite` `Set.Iic` `PartialOrder.toPreorder`	`CovBy` `Preorder.toLT`	—	`toDual_covBy_toDual_iff` `exists_covby_infinite_Ici_of_infinite_Ici` `instIsStronglyAtomicOrderDualOfIsStronglyCoatomic`
`instIsStronglyAtomic` 📖	mathematical	—	`IsStronglyAtomic`	—	`Finset.exists_minimal` `instIsTransLe` `LT.lt.not_ge` `LE.le.trans` `LT.lt.le`
`instIsStronglyCoatomic` 📖	mathematical	—	`IsStronglyCoatomic`	—	`isStronglyAtomic_dual_iff_is_stronglyCoatomic` `instIsStronglyAtomic`

---

← Back to Index