Documentation Verification Report

PropInstances

📁 Source: Mathlib/Order/PropInstances.lean

Statistics

Metric	Count
Definitions `decidablePredBot`, `decidablePredTop`, `decidableRelBot`, `decidableRelTop`, `instBoundedOrder`, `instDistribLattice`, `linearOrder`	7
Theorems `codisjoint_iff`, `disjoint_iff`, `isCompl_iff`, `bot_eq_false`, `codisjoint_iff`, `disjoint_iff`, `isCompl_iff`, `le_total`, `top_eq_true`, `inf_Prop_eq`, `sup_Prop_eq`	11
Total	18

Pi

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`codisjoint_iff` 📖	mathematical	—	`Codisjoint` `partialOrder` `instOrderTop` `Preorder.toLE` `PartialOrder.toPreorder`	—	`disjoint_iff`
`disjoint_iff` 📖	mathematical	—	`Disjoint` `partialOrder` `instOrderBot` `Preorder.toLE` `PartialOrder.toPreorder`	—	`update_le_iff` `bot_le`
`isCompl_iff` 📖	mathematical	—	`IsCompl` `partialOrder` `instBoundedOrder` `Preorder.toLE` `PartialOrder.toPreorder`	—	—

Prop

Definitions

Name	Category	Theorems
`decidablePredBot` 📖	CompOp	—
`decidablePredTop` 📖	CompOp	1 math math: `Matrix.toBlock_mul_eq_mul`
`decidableRelBot` 📖	CompOp	—
`decidableRelTop` 📖	CompOp	—
`instBoundedOrder` 📖	CompOp	8 math math: `codisjoint_iff`, `bot_eq_false`, `isCompl_iff`, `Set.setOf_bot`, `disjoint_iff`, `instIsSimpleOrderProp`, `Set.setOf_top`, `top_eq_true`
`instDistribLattice` 📖	CompOp	2 math math: `inf_Prop_eq`, `sup_Prop_eq`
`linearOrder` 📖	CompOp	2 math math: `Multiset.map_count_True_eq_filter_card`, `Fintype.univ_Prop`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bot_eq_false` 📖	mathematical	—	`Bot.bot` `OrderBot.toBot` `le` `BoundedOrder.toOrderBot` `instBoundedOrder`	—	—
`codisjoint_iff` 📖	mathematical	—	`Codisjoint` `partialOrder` `BoundedOrder.toOrderTop` `Preorder.toLE` `PartialOrder.toPreorder` `instBoundedOrder`	—	`codisjoint_iff_le_sup`
`disjoint_iff` 📖	mathematical	—	`Disjoint` `partialOrder` `BoundedOrder.toOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `instBoundedOrder`	—	`disjoint_iff_inf_le`
`isCompl_iff` 📖	mathematical	—	`IsCompl` `partialOrder` `instBoundedOrder`	—	`isCompl_iff` `disjoint_iff` `codisjoint_iff` `not_iff`
`le_total` 📖	mathematical	—	`le`	—	`instIsEmptyFalse`
`top_eq_true` 📖	mathematical	—	`Top.top` `OrderTop.toTop` `le` `BoundedOrder.toOrderTop` `instBoundedOrder`	—	—

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`inf_Prop_eq` 📖	mathematical	—	`SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `Prop.instDistribLattice`	—	—
`sup_Prop_eq` 📖	mathematical	—	`SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `DistribLattice.toLattice` `Prop.instDistribLattice`	—	—

---

← Back to Index