Documentation Verification Report

Prod

📁 Source: Mathlib/Data/Finset/Lattice/Prod.lean

Statistics

Metric	Count
Definitions	0
Theorems `inf'_prodMap`, `inf'_product_left`, `inf'_product_right`, `inf'_sup_inf'`, `inf_prodMap`, `inf_product_left`, `inf_product_right`, `inf_sup_inf`, `prodMk_inf'_inf'`, `prodMk_sup'_sup'`, `sup'_inf_sup'`, `sup'_prodMap`, `sup'_product_left`, `sup'_product_right`, `sup_inf_sup`, `sup_prodMap`, `sup_product_left`, `sup_product_right`	18
Total	18

Finset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`inf'_prodMap` 📖	mathematical	`Nonempty` `SProd.sprod` `Finset` `instSProd`	`inf'` `Prod.instSemilatticeInf` `Nonempty.fst` `Nonempty.snd`	—	`Nonempty.fst` `Nonempty.snd` `Nonempty.product` `prodMk_inf'_inf'`
`inf'_product_left` 📖	mathematical	`Nonempty` `SProd.sprod` `Finset` `instSProd`	`inf'` `Nonempty.fst` `Nonempty.snd`	—	`sup'_product_left`
`inf'_product_right` 📖	mathematical	`Nonempty` `SProd.sprod` `Finset` `instSProd`	`inf'` `Nonempty.snd` `Nonempty.fst`	—	`sup'_product_right`
`inf'_sup_inf'` 📖	mathematical	`Nonempty`	`SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `DistribLattice.toLattice` `inf'` `Lattice.toSemilatticeInf` `SProd.sprod` `Finset` `instSProd` `Nonempty.product`	—	`sup'_inf_sup'`
`inf_prodMap` 📖	mathematical	`Nonempty`	`inf` `Prod.instSemilatticeInf` `Prod.instOrderTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `SProd.sprod` `Finset` `instSProd`	—	`sup_prodMap`
`inf_product_left` 📖	mathematical	—	`inf` `SProd.sprod` `Finset` `instSProd`	—	`sup_product_left`
`inf_product_right` 📖	mathematical	—	`inf` `SProd.sprod` `Finset` `instSProd`	—	`sup_product_right`
`inf_sup_inf` 📖	mathematical	—	`SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `DistribLattice.toLattice` `inf` `Lattice.toSemilatticeInf` `SProd.sprod` `Finset` `instSProd`	—	`sup_inf_sup`
`prodMk_inf'_inf'` 📖	mathematical	`Nonempty`	`inf'` `Prod.instSemilatticeInf` `SProd.sprod` `Finset` `instSProd` `Nonempty.product`	—	`prodMk_sup'_sup'`
`prodMk_sup'_sup'` 📖	mathematical	`Nonempty`	`sup'` `Prod.instSemilatticeSup` `SProd.sprod` `Finset` `instSProd` `Nonempty.product`	—	`eq_of_forall_ge_iff` `Nonempty.product` `sup'_congr`
`sup'_inf_sup'` 📖	mathematical	`Nonempty`	`SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `sup'` `Lattice.toSemilatticeSup` `SProd.sprod` `Finset` `instSProd` `Nonempty.product`	—	`Nonempty.product` `sup'_inf_distrib_right` `sup'_congr` `sup'_inf_distrib_left` `Nonempty.fst` `Nonempty.snd` `sup'_product_left`
`sup'_prodMap` 📖	mathematical	`Nonempty` `SProd.sprod` `Finset` `instSProd`	`sup'` `Prod.instSemilatticeSup` `Nonempty.fst` `Nonempty.snd`	—	`Nonempty.fst` `Nonempty.snd` `Nonempty.product` `prodMk_sup'_sup'`
`sup'_product_left` 📖	mathematical	`Nonempty` `SProd.sprod` `Finset` `instSProd`	`sup'` `Nonempty.fst` `Nonempty.snd`	—	`eq_of_forall_ge_iff` `Nonempty.fst` `Nonempty.snd` `forall_swap`
`sup'_product_right` 📖	mathematical	`Nonempty` `SProd.sprod` `Finset` `instSProd`	`sup'` `Nonempty.snd` `Nonempty.fst`	—	`Nonempty.snd` `Nonempty.fst` `sup'_product_left` `sup'_comm`
`sup_inf_sup` 📖	mathematical	—	`SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `sup` `Lattice.toSemilatticeSup` `SProd.sprod` `Finset` `instSProd`	—	`sup_inf_distrib_right` `sup_inf_distrib_left` `sup_product_left`
`sup_prodMap` 📖	mathematical	`Nonempty`	`sup` `Prod.instSemilatticeSup` `Prod.instOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `SProd.sprod` `Finset` `instSProd`	—	`eq_of_forall_ge_iff`
`sup_product_left` 📖	mathematical	—	`sup` `SProd.sprod` `Finset` `instSProd`	—	`eq_of_forall_ge_iff` `forall_swap`
`sup_product_right` 📖	mathematical	—	`sup` `SProd.sprod` `Finset` `instSProd`	—	`sup_product_left` `sup_comm`

---

← Back to Index