Pi

Statistics

Name	Kind	Assumes	Proves	Validates	Depends On
`inf_sup` 📖	mathematical	—	`inf` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `BoundedOrder.toOrderTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `sup` `Lattice.toSemilatticeSup` `BoundedOrder.toOrderBot` `SemilatticeSup.toPartialOrder` `pi` `Finset` `instMembership` `attach`	—	`induction` `sup_singleton` `inf_insert` `mem_insert_self` `mem_insert_of_mem` `attach_insert` `sup_inf_sup` `eq_of_forall_ge_iff` `inf_image` `mem_of_mem_insert_of_ne` `mem_insert`
`sup_inf` 📖	mathematical	—	`sup` `Lattice.toSemilatticeSup` `DistribLattice.toLattice` `BoundedOrder.toOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `inf` `Lattice.toSemilatticeInf` `BoundedOrder.toOrderTop` `SemilatticeInf.toPartialOrder` `pi` `Finset` `instMembership` `attach`	—	`inf_sup`

---