Lattice

📁 Source: Mathlib/Data/Multiset/Lattice.lean

Statistics

Metric	Count
Definitions `inf`, `sup`	2
Theorems `inf_add`, `inf_coe`, `inf_cons`, `inf_dedup`, `inf_le`, `inf_mono`, `inf_ndinsert`, `inf_ndunion`, `inf_singleton`, `inf_union`, `inf_zero`, `le_inf`, `le_sup`, `nodup_sup_iff`, `sup_add`, `sup_coe`, `sup_cons`, `sup_dedup`, `sup_le`, `sup_mono`, `sup_ndinsert`, `sup_ndunion`, `sup_singleton`, `sup_union`, `sup_zero`	25
Total	27

Multiset

Definitions

Name	Category	Theorems
`inf` 📖	CompOp	16 math math: `inf_dedup`, `le_inf`, `inf_le`, `untrop_sum`, `inf_zero`, `inf_add`, `Finset.inf_def`, `inf_coe`, `trop_inf`, `inf_ndunion`, `inf_cons`, `inf_mono`, `inf_union`, `inf_singleton`, `Ideal.multiset_prod_le_inf`, `inf_ndinsert`
`sup` 📖	CompOp	17 math math: `sup_ndinsert`, `sup_cons`, `sup_zero`, `le_sup`, `support_sum_subset`, `sup_singleton`, `sup_coe`, `mem_sup_map_support_iff`, `sup_dedup`, `nodup_sup_iff`, `sup_ndunion`, `support_sum_eq`, `sup_le`, `Finset.sup_def`, `sup_union`, `sup_mono`, `sup_add`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`inf_add` 📖	mathematical	—	`inf` `Multiset` `instAdd` `SemilatticeInf.toMin`	—	`instCommutativeMin_mathlib` `instAssociativeMin_mathlib` `fold.congr_simp` `inf_of_le_left` `le_refl` `fold_add`
`inf_coe` 📖	mathematical	—	`inf` `ofList` `SemilatticeInf.toMin` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder`	—	—
`inf_cons` 📖	mathematical	—	`inf` `cons` `SemilatticeInf.toMin`	—	`fold_cons_left` `instCommutativeMin_mathlib` `instAssociativeMin_mathlib`
`inf_dedup` 📖	mathematical	—	`inf` `dedup`	—	`fold_dedup_idem` `instCommutativeMin_mathlib` `instAssociativeMin_mathlib` `instIdempotentOpMin_mathlib`
`inf_le` 📖	mathematical	`Multiset` `instMembership`	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `inf`	—	`le_inf` `le_rfl`
`inf_mono` 📖	mathematical	`Multiset` `instHasSubset`	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `inf`	—	`le_inf` `inf_le`
`inf_ndinsert` 📖	mathematical	—	`inf` `ndinsert` `SemilatticeInf.toMin`	—	`inf_dedup` `dedup_ext` `mem_ndinsert` `mem_cons` `inf_cons`
`inf_ndunion` 📖	mathematical	—	`inf` `ndunion` `SemilatticeInf.toMin`	—	`inf_dedup` `dedup_ext` `mem_ndunion` `mem_add` `inf_add`
`inf_singleton` 📖	mathematical	—	`inf` `Multiset` `instSingleton`	—	`inf_top_eq`
`inf_union` 📖	mathematical	—	`inf` `Multiset` `instUnion` `SemilatticeInf.toMin`	—	`inf_dedup` `dedup_ext` `mem_union` `mem_add` `inf_add`
`inf_zero` 📖	mathematical	—	`inf` `Multiset` `instZero` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder`	—	`fold_zero` `instCommutativeMin_mathlib` `instAssociativeMin_mathlib`
`le_inf` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `inf`	—	`induction_on` `inf_zero` `le_top` `notMem_zero` `IsEmpty.forall_iff` `instIsEmptyFalse` `inf_cons` `le_inf_iff` `mem_cons`
`le_sup` 📖	mathematical	`Multiset` `instMembership`	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `sup`	—	`sup_le` `le_rfl`
`nodup_sup_iff` 📖	mathematical	—	`Nodup` `sup` `Multiset` `Lattice.toSemilatticeSup` `instLattice` `instOrderBot`	—	`induction_on` `sup_zero` `instIsEmptyFalse` `sup_cons`
`sup_add` 📖	mathematical	—	`sup` `Multiset` `instAdd` `SemilatticeSup.toMax`	—	`instCommutativeMax_mathlib` `instAssociativeMax_mathlib` `fold.congr_simp` `sup_of_le_left` `fold_add`
`sup_coe` 📖	mathematical	—	`sup` `ofList` `SemilatticeSup.toMax` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder`	—	—
`sup_cons` 📖	mathematical	—	`sup` `cons` `SemilatticeSup.toMax`	—	`fold_cons_left` `instCommutativeMax_mathlib` `instAssociativeMax_mathlib`
`sup_dedup` 📖	mathematical	—	`sup` `dedup`	—	`fold_dedup_idem` `instCommutativeMax_mathlib` `instAssociativeMax_mathlib` `instIdempotentOpMax_mathlib`
`sup_le` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `sup`	—	`induction_on` `sup_zero` `instIsEmptyFalse` `sup_cons`
`sup_mono` 📖	mathematical	`Multiset` `instHasSubset`	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `sup`	—	`sup_le` `le_sup`
`sup_ndinsert` 📖	mathematical	—	`sup` `ndinsert` `SemilatticeSup.toMax`	—	`sup_dedup` `dedup_ext` `sup_cons`
`sup_ndunion` 📖	mathematical	—	`sup` `ndunion` `SemilatticeSup.toMax`	—	`sup_dedup` `dedup_ext` `sup_add`
`sup_singleton` 📖	mathematical	—	`sup` `Multiset` `instSingleton`	—	`sup_bot_eq`
`sup_union` 📖	mathematical	—	`sup` `Multiset` `instUnion` `SemilatticeSup.toMax`	—	`sup_dedup` `dedup_ext` `sup_add`
`sup_zero` 📖	mathematical	—	`sup` `Multiset` `instZero` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder`	—	`fold_zero` `instCommutativeMax_mathlib` `instAssociativeMax_mathlib`

---

← Back to Index