PartialSups

Statistics

Metric	Count
Definitions	0
Theorems `partialSups_add_one`, `partialSups_add_one'`, `partialSups_succ'`	3
Total	3

Name	Kind	Assumes	Proves	Validates	Depends On
`partialSups_add_one` 📖	mathematical	—	`DFunLike.coe` `OrderHom` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SemilatticeSup.toPartialOrder` `OrderHom.instFunLike` `partialSups` `SemilatticeSup.toMax`	—	`partialSups_succ` `Order.succ_eq_add_one`
`partialSups_add_one'` 📖	mathematical	—	`DFunLike.coe` `OrderHom` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SemilatticeSup.toPartialOrder` `OrderHom.instFunLike` `partialSups` `LocallyFiniteOrder.toLocallyFiniteOrderBot` `SemilatticeSup.toMax` `Bot.bot` `OrderBot.toBot` `Preorder.toLE`	—	`partialSups_succ` `partialSups_succ'`
`partialSups_succ'` 📖	mathematical	—	`DFunLike.coe` `OrderHom` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SemilatticeSup.toPartialOrder` `OrderHom.instFunLike` `partialSups` `LocallyFiniteOrder.toLocallyFiniteOrderBot` `Order.succ` `SemilatticeSup.toMax` `Bot.bot` `OrderBot.toBot` `Preorder.toLE`	—	`LinearLocallyFiniteOrder.instIsSuccArchimedeanOfLocallyFiniteOrder` `partialSups_succ` `partialSups_bot` `sup_assoc` `bot_le`

---