Documentation Verification Report

BigOperators

📁 Source: Mathlib/Algebra/Tropical/BigOperators.lean

Statistics

Metric	Count
Definitions	0
Theorems `trop_inf`, `untrop_sum`, `untrop_sum'`, `trop_minimum`, `trop_sum`, `untrop_prod`, `trop_inf`, `trop_sum`, `untrop_prod`, `untrop_sum`, `trop_iInf`, `trop_sInf_image`, `trop_sum`, `untrop_prod`, `untrop_sum`, `untrop_sum_eq_sInf_image`	16
Total	16

Finset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`trop_inf` 📖	mathematical	—	`Tropical.trop` `inf` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `sum` `Tropical` `Tropical.instAddCommMonoidTropical`	—	`Multiset.map_map` `Multiset.map_congr` `Multiset.trop_inf`
`untrop_sum` 📖	mathematical	—	`Tropical.untrop` `WithTop` `sum` `Tropical` `Tropical.instAddCommMonoidTropical` `WithTop.linearOrder` `ConditionallyCompleteLinearOrder.toLinearOrder` `WithTop.instOrderTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `iInf` `Finset` `SetLike.instMembership` `instSetLike` `WithTop.instInfSet` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf`	—	`sum_attach`
`untrop_sum'` 📖	mathematical	—	`Tropical.untrop` `sum` `Tropical` `Tropical.instAddCommMonoidTropical` `inf` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`Multiset.map_congr` `Multiset.map_map` `Multiset.untrop_sum`

List

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`trop_minimum` 📖	mathematical	—	`Tropical.trop` `WithTop` `minimum` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `LinearOrder.toDecidableLT` `Tropical` `Tropical.instAdd` `WithTop.linearOrder` `Tropical.instZeroTropical` `WithTop.top` `WithTop.some`	—	`minimum_cons`
`trop_sum` 📖	mathematical	—	`Tropical.trop` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Tropical` `Tropical.instMulOfAdd` `Tropical.instOneTropical`	—	—
`untrop_prod` 📖	mathematical	—	`Tropical.untrop` `Tropical` `Tropical.instMulOfAdd` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `Tropical.instOneTropical` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	—	—

Multiset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`trop_inf` 📖	mathematical	—	`Tropical.trop` `inf` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `sum` `Tropical` `Tropical.instAddCommMonoidTropical` `map`	—	`induction` `inf_zero` `inf_cons` `map_cons` `sum_cons`
`trop_sum` 📖	mathematical	—	`Tropical.trop` `sum` `prod` `Tropical` `Tropical.instCommMonoidTropical` `map`	—	`List.trop_sum`
`untrop_prod` 📖	mathematical	—	`Tropical.untrop` `prod` `Tropical` `Tropical.instCommMonoidTropical` `sum` `map`	—	`List.untrop_prod`
`untrop_sum` 📖	mathematical	—	`Tropical.untrop` `sum` `Tropical` `Tropical.instAddCommMonoidTropical` `inf` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `map`	—	`induction` `inf_zero` `sum_cons` `map_cons` `inf_cons`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`trop_iInf` 📖	mathematical	—	`Tropical.trop` `WithTop` `iInf` `WithTop.instInfSet` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `Finset.sum` `Tropical` `Tropical.instAddCommMonoidTropical` `WithTop.linearOrder` `ConditionallyCompleteLinearOrder.toLinearOrder` `WithTop.instOrderTop` `Preorder.toLE` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Finset.univ`	—	`iInf.eq_1` `Set.image_univ` `Finset.coe_univ` `trop_sInf_image`
`trop_sInf_image` 📖	mathematical	—	`Tropical.trop` `WithTop` `InfSet.sInf` `WithTop.instInfSet` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `Set.image` `SetLike.coe` `Finset` `Finset.instSetLike` `Finset.sum` `Tropical` `Tropical.instAddCommMonoidTropical` `WithTop.linearOrder` `ConditionallyCompleteLinearOrder.toLinearOrder` `WithTop.instOrderTop` `Preorder.toLE` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`Finset.eq_empty_or_nonempty` `Finset.coe_empty` `Set.image_empty` `WithTop.sInf_empty` `Finset.inf'_eq_csInf_image` `Finset.inf'_eq_inf` `Finset.trop_inf`
`trop_sum` 📖	mathematical	—	`Tropical.trop` `Finset.sum` `Finset.prod` `Tropical` `Tropical.instCommMonoidTropical`	—	`Multiset.map_map` `Multiset.map_congr` `Multiset.trop_sum`
`untrop_prod` 📖	mathematical	—	`Tropical.untrop` `Finset.prod` `Tropical` `Tropical.instCommMonoidTropical` `Finset.sum`	—	`Multiset.map_map` `Multiset.map_congr` `Multiset.untrop_prod`
`untrop_sum` 📖	mathematical	—	`Tropical.untrop` `WithTop` `Finset.sum` `Tropical` `Tropical.instAddCommMonoidTropical` `WithTop.linearOrder` `ConditionallyCompleteLinearOrder.toLinearOrder` `WithTop.instOrderTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Finset.univ` `iInf` `WithTop.instInfSet` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf`	—	`iInf.eq_1` `Set.image_univ` `Finset.coe_univ` `untrop_sum_eq_sInf_image`
`untrop_sum_eq_sInf_image` 📖	mathematical	—	`Tropical.untrop` `WithTop` `Finset.sum` `Tropical` `Tropical.instAddCommMonoidTropical` `WithTop.linearOrder` `ConditionallyCompleteLinearOrder.toLinearOrder` `WithTop.instOrderTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `InfSet.sInf` `WithTop.instInfSet` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `Set.image` `SetLike.coe` `Finset` `Finset.instSetLike`	—	`Finset.eq_empty_or_nonempty` `Finset.coe_empty` `Set.image_empty` `WithTop.sInf_empty` `Finset.inf'_eq_csInf_image` `Finset.inf'_eq_inf` `Finset.untrop_sum'`

---

← Back to Index