Documentation Verification Report

Quantale

📁 Source: Mathlib/Algebra/Order/Quantale.lean

Statistics

Metric	Count
Definitions `AddQuantale`, `leftAddResiduation`, `rightAddResiduation`, `«term_⇨ᵣ_»`, `«term_⇨ₗ_»`, `IsAddQuantale`, `IsQuantale`, `Quantale`, `leftMulResiduation`, `rightMulResiduation`, `«term_⇨ᵣ_»`, `«term_⇨ₗ_»`	12
Theorems `add_bot`, `add_iSup_distrib`, `add_sup_distrib`, `bot_add`, `iSup_add_distrib`, `instAddLeftMono`, `instAddRightMono`, `leftAddResiduation_le_iff_add_le`, `rightAddResiduation_le_iff_add_le`, `sup_add_distrib`, `add_sSup_distrib`, `sSup_add_distrib`, `mul_sSup_distrib`, `sSup_mul_distrib`, `bot_mul`, `iSup_mul_distrib`, `instMulLeftMono`, `instMulRightMono`, `leftMulResiduation_le_iff_mul_le`, `mul_bot`, `mul_iSup_distrib`, `mul_sup_distrib`, `rightMulResiduation_le_iff_mul_le`, `sup_mul_distrib`, `add_sSup_distrib`, `mul_sSup_distrib`, `sSup_add_distrib`, `sSup_mul_distrib`	28
Total	40

AddQuantale

Definitions

Name	Category	Theorems
`leftAddResiduation` 📖	CompOp	1 math math: `leftAddResiduation_le_iff_add_le`
`rightAddResiduation` 📖	CompOp	1 math math: `rightAddResiduation_le_iff_add_le`
`«term_⇨ᵣ_»` 📖	CompOp	—
`«term_⇨ₗ_»` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_bot` 📖	mathematical	—	`AddSemigroup.toAdd` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder`	—	`sSup_empty` `add_sSup_distrib` `iSup_congr_Prop` `Set.mem_empty_iff_false` `iSup_neg` `iSup_bot`
`add_iSup_distrib` 📖	mathematical	—	`AddSemigroup.toAdd` `iSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup`	—	`iSup.eq_1` `add_sSup_distrib` `iSup_range`
`add_sup_distrib` 📖	mathematical	—	`AddSemigroup.toAdd` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice`	—	`iSup_pair` `sSup_pair` `add_sSup_distrib`
`bot_add` 📖	mathematical	—	`AddSemigroup.toAdd` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder`	—	`sSup_empty` `sSup_add_distrib` `iSup_congr_Prop` `Set.mem_empty_iff_false` `iSup_neg` `iSup_bot`
`iSup_add_distrib` 📖	mathematical	—	`AddSemigroup.toAdd` `iSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup`	—	`iSup.eq_1` `sSup_add_distrib` `iSup_range`
`instAddLeftMono` 📖	mathematical	—	`AddLeftMono` `AddSemigroup.toAdd` `Preorder.toLE` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf`	—	`left_eq_sup` `add_sup_distrib` `sup_of_le_left`
`instAddRightMono` 📖	mathematical	—	`AddRightMono` `AddSemigroup.toAdd` `Preorder.toLE` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf`	—	`left_eq_sup` `sup_add_distrib` `sup_of_le_left`
`leftAddResiduation_le_iff_add_le` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `leftAddResiduation` `AddSemigroup.toAdd`	—	`le_imp_le_of_le_of_le` `add_le_add_left` `instAddRightMono` `le_refl` `sSup_add_distrib` `iSup_le_iff` `le_sSup`
`rightAddResiduation_le_iff_add_le` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `rightAddResiduation` `AddSemigroup.toAdd`	—	`le_imp_le_of_le_of_le` `add_le_add_right` `instAddLeftMono` `le_refl` `add_sSup_distrib` `iSup_le_iff` `le_sSup`
`sup_add_distrib` 📖	mathematical	—	`AddSemigroup.toAdd` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice`	—	`iSup_pair` `sSup_pair` `sSup_add_distrib`

IsAddQuantale

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_sSup_distrib` 📖	mathematical	—	`AddSemigroup.toAdd` `SupSet.sSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `iSup` `Set` `Set.instMembership`	—	—
`sSup_add_distrib` 📖	mathematical	—	`AddSemigroup.toAdd` `SupSet.sSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `iSup` `Set` `Set.instMembership`	—	—

IsQuantale

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mul_sSup_distrib` 📖	mathematical	—	`Semigroup.toMul` `SupSet.sSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `iSup` `Set` `Set.instMembership`	—	—
`sSup_mul_distrib` 📖	mathematical	—	`Semigroup.toMul` `SupSet.sSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `iSup` `Set` `Set.instMembership`	—	—

Quantale

Definitions

Name	Category	Theorems
`leftMulResiduation` 📖	CompOp	1 math math: `leftMulResiduation_le_iff_mul_le`
`rightMulResiduation` 📖	CompOp	1 math math: `rightMulResiduation_le_iff_mul_le`
`«term_⇨ᵣ_»` 📖	CompOp	—
`«term_⇨ₗ_»` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bot_mul` 📖	mathematical	—	`Semigroup.toMul` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder`	—	`sSup_empty` `sSup_mul_distrib` `iSup_congr_Prop` `iSup_neg` `iSup_bot`
`iSup_mul_distrib` 📖	mathematical	—	`Semigroup.toMul` `iSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup`	—	`iSup.eq_1` `sSup_mul_distrib` `iSup_range`
`instMulLeftMono` 📖	mathematical	—	`MulLeftMono` `Semigroup.toMul` `Preorder.toLE` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf`	—	`left_eq_sup` `mul_sup_distrib` `sup_of_le_left`
`instMulRightMono` 📖	mathematical	—	`MulRightMono` `Semigroup.toMul` `Preorder.toLE` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf`	—	`left_eq_sup` `sup_mul_distrib` `sup_of_le_left`
`leftMulResiduation_le_iff_mul_le` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `leftMulResiduation` `Semigroup.toMul`	—	`le_imp_le_of_le_of_le` `mul_le_mul_left` `instMulRightMono` `le_refl` `sSup_mul_distrib` `le_sSup`
`mul_bot` 📖	mathematical	—	`Semigroup.toMul` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder`	—	`sSup_empty` `mul_sSup_distrib` `iSup_congr_Prop` `iSup_neg` `iSup_bot`
`mul_iSup_distrib` 📖	mathematical	—	`Semigroup.toMul` `iSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup`	—	`iSup.eq_1` `mul_sSup_distrib` `iSup_range`
`mul_sup_distrib` 📖	mathematical	—	`Semigroup.toMul` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice`	—	`iSup_pair` `sSup_pair` `mul_sSup_distrib`
`rightMulResiduation_le_iff_mul_le` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `rightMulResiduation` `Semigroup.toMul`	—	`le_imp_le_of_le_of_le` `mul_le_mul_right` `instMulLeftMono` `le_refl` `mul_sSup_distrib` `le_sSup`
`sup_mul_distrib` 📖	mathematical	—	`Semigroup.toMul` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice`	—	`iSup_pair` `sSup_pair` `sSup_mul_distrib`

(root)

Definitions

Name	Category	Theorems
`AddQuantale` 📖	CompData	—
`IsAddQuantale` 📖	CompData	—
`IsQuantale` 📖	CompData	—
`Quantale` 📖	CompData	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_sSup_distrib` 📖	mathematical	—	`AddSemigroup.toAdd` `SupSet.sSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `iSup` `Set` `Set.instMembership`	—	`IsAddQuantale.add_sSup_distrib`
`mul_sSup_distrib` 📖	mathematical	—	`Semigroup.toMul` `SupSet.sSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `iSup` `Set` `Set.instMembership`	—	`IsQuantale.mul_sSup_distrib`
`sSup_add_distrib` 📖	mathematical	—	`AddSemigroup.toAdd` `SupSet.sSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `iSup` `Set` `Set.instMembership`	—	`IsAddQuantale.sSup_add_distrib`
`sSup_mul_distrib` 📖	mathematical	—	`Semigroup.toMul` `SupSet.sSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `iSup` `Set` `Set.instMembership`	—	`IsQuantale.sSup_mul_distrib`

---

← Back to Index