FinsetOps

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

Statistics

Metric	Count
Definitions `ndinsert`, `ndinter`, `ndunion`	3
Theorems `ndinter_eq_zero`, `ndunion_eq`, `inter`, `ndinsert`, `ndinter`, `ndunion`, `ndinter_eq_left`, `ndunion_eq_right`, `attach_ndinsert`, `coe_ndinsert`, `coe_ndinter`, `coe_ndunion`, `cons_ndinter_of_mem`, `cons_ndunion`, `dedup_add`, `dedup_cons`, `disjoint_ndinsert_left`, `disjoint_ndinsert_right`, `inter_le_ndinter`, `le_ndinsert_self`, `le_ndinter`, `le_ndunion_left`, `le_ndunion_right`, `length_ndinsert_of_mem`, `length_ndinsert_of_notMem`, `mem_ndinsert`, `mem_ndinsert_of_mem`, `mem_ndinsert_self`, `mem_ndinter`, `mem_ndunion`, `ndinsert_le`, `ndinsert_of_mem`, `ndinsert_of_notMem`, `ndinsert_zero`, `ndinter_cons_of_notMem`, `ndinter_eq_inter`, `ndinter_eq_zero_iff_disjoint`, `ndinter_le_left`, `ndinter_le_right`, `ndinter_subset_left`, `ndinter_subset_right`, `ndunion_eq_union`, `ndunion_le`, `ndunion_le_add`, `ndunion_le_union`, `subset_ndunion_left`, `subset_ndunion_right`, `zero_ndinter`, `zero_ndunion`	49
Total	52

Multiset

Definitions

Name	Category	Theorems
`ndinsert` 📖	CompOp	23 math math: `sup_ndinsert`, `Finset.insert_val`, `dedup_cons`, `ndinsert_of_notMem`, `attach_ndinsert`, `Finset.insert_def`, `le_ndinsert_self`, `mem_ndinsert`, `length_ndinsert_of_notMem`, `ndinsert_zero`, `coe_ndinsert`, `cons_ndunion`, `gcd_ndinsert`, `length_ndinsert_of_mem`, `disjoint_ndinsert_right`, `lcm_ndinsert`, `Nodup.ndinsert`, `ndinsert_le`, `mem_ndinsert_of_mem`, `ndinsert_of_mem`, `disjoint_ndinsert_left`, `mem_ndinsert_self`, `inf_ndinsert`
`ndinter` 📖	CompOp	17 math math: `Subset.ndinter_eq_left`, `Nodup.ndinter`, `ndinter_cons_of_notMem`, `coe_ndinter`, `ndinter_le_left`, `le_ndinter`, `inter_le_ndinter`, `zero_ndinter`, `Finset.inter_val_nd`, `ndinter_subset_left`, `ndinter_eq_inter`, `ndinter_subset_right`, `Disjoint.ndinter_eq_zero`, `ndinter_le_right`, `cons_ndinter_of_mem`, `ndinter_eq_zero_iff_disjoint`, `mem_ndinter`
`ndunion` 📖	CompOp	21 math math: `Nodup.ndunion`, `ndunion_le_union`, `zero_ndunion`, `ndunion_eq_union`, `subset_ndunion_left`, `dedup_add`, `gcd_ndunion`, `Disjoint.ndunion_eq`, `Finset.union_val_nd`, `cons_ndunion`, `mem_ndunion`, `coe_ndunion`, `ndunion_le`, `subset_ndunion_right`, `Subset.ndunion_eq_right`, `inf_ndunion`, `ndunion_le_add`, `sup_ndunion`, `le_ndunion_left`, `lcm_ndunion`, `le_ndunion_right`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`attach_ndinsert` 📖	mathematical	—	`attach` `ndinsert` `Multiset` `instMembership` `mem_ndinsert_self` `map` `mem_ndinsert_of_mem`	—	`mem_ndinsert_self` `mem_ndinsert_of_mem` `map_id` `ndinsert_of_mem` `mem_attach` `mem_cons_self` `mem_cons_of_mem` `attach_cons` `ndinsert_of_notMem`
`coe_ndinsert` 📖	mathematical	—	`ndinsert` `ofList` `List.instInsertOfDecidableEq_mathlib`	—	—
`coe_ndinter` 📖	mathematical	—	`ndinter` `ofList`	—	`filter_congr`
`coe_ndunion` 📖	mathematical	—	`ndunion` `ofList`	—	—
`cons_ndinter_of_mem` 📖	mathematical	`Multiset` `instMembership`	`ndinter` `cons`	—	`filter_cons_of_pos`
`cons_ndunion` 📖	mathematical	—	`ndunion` `cons` `ndinsert`	—	`Quot.induction_on₂`
`dedup_add` 📖	mathematical	—	`dedup` `Multiset` `instAdd` `ndunion`	—	`Quot.induction_on₂` `List.dedup_append`
`dedup_cons` 📖	mathematical	—	`dedup` `cons` `ndinsert`	—	`dedup_cons_of_mem` `ndinsert_of_mem` `dedup_cons_of_notMem` `ndinsert_of_notMem`
`disjoint_ndinsert_left` 📖	mathematical	—	`Disjoint` `Multiset` `instPartialOrder` `instOrderBot` `ndinsert` `instMembership`	—	`disjoint_cons_left`
`disjoint_ndinsert_right` 📖	mathematical	—	`Disjoint` `Multiset` `instPartialOrder` `instOrderBot` `ndinsert` `instMembership`	—	`disjoint_comm` `disjoint_ndinsert_left`
`inter_le_ndinter` 📖	mathematical	—	`Multiset` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `instInter` `ndinter`	—	`le_ndinter` `inter_le_left` `subset_of_le` `inter_le_right`
`le_ndinsert_self` 📖	mathematical	—	`Multiset` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `ndinsert`	—	`List.sublist_insert`
`le_ndinter` 📖	mathematical	—	`Multiset` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `ndinter` `instHasSubset`	—	—
`le_ndunion_left` 📖	mathematical	`Nodup`	`Multiset` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `ndunion`	—	`le_iff_subset` `subset_ndunion_left`
`le_ndunion_right` 📖	mathematical	—	`Multiset` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `ndunion`	—	`Quot.induction_on₂` `List.suffix_union_right`
`length_ndinsert_of_mem` 📖	mathematical	`Multiset` `instMembership`	`card` `ndinsert`	—	`ndinsert_of_mem`
`length_ndinsert_of_notMem` 📖	mathematical	`Multiset` `instMembership`	`card` `ndinsert`	—	`ndinsert_of_notMem` `card_cons`
`mem_ndinsert` 📖	mathematical	—	`Multiset` `instMembership` `ndinsert`	—	—
`mem_ndinsert_of_mem` 📖	mathematical	`Multiset` `instMembership`	`ndinsert`	—	`mem_ndinsert`
`mem_ndinsert_self` 📖	mathematical	—	`Multiset` `instMembership` `ndinsert`	—	—
`mem_ndinter` 📖	mathematical	—	`Multiset` `instMembership` `ndinter`	—	—
`mem_ndunion` 📖	mathematical	—	`Multiset` `instMembership` `ndunion`	—	`Quot.induction_on₂`
`ndinsert_le` 📖	mathematical	—	`Multiset` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `ndinsert` `instMembership`	—	`le_trans` `le_ndinsert_self` `mem_of_le` `mem_ndinsert_self` `ndinsert_of_mem` `ndinsert_of_notMem` `cons_erase` `cons_le_cons_iff` `le_cons_of_notMem`
`ndinsert_of_mem` 📖	mathematical	`Multiset` `instMembership`	`ndinsert`	—	—
`ndinsert_of_notMem` 📖	mathematical	`Multiset` `instMembership`	`ndinsert` `cons`	—	—
`ndinsert_zero` 📖	mathematical	—	`ndinsert` `Multiset` `instZero` `instSingleton`	—	—
`ndinter_cons_of_notMem` 📖	mathematical	`Multiset` `instMembership`	`ndinter` `cons`	—	`filter_cons_of_neg`
`ndinter_eq_inter` 📖	mathematical	`Nodup`	`ndinter` `Multiset` `instInter`	—	`le_antisymm` `le_inter` `ndinter_le_left` `ndinter_le_right` `inter_le_ndinter`
`ndinter_eq_zero_iff_disjoint` 📖	mathematical	—	`ndinter` `Multiset` `instZero` `Disjoint` `instPartialOrder` `instOrderBot`	—	`subset_zero`
`ndinter_le_left` 📖	mathematical	—	`Multiset` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `ndinter`	—	`le_ndinter` `le_rfl`
`ndinter_le_right` 📖	mathematical	`Nodup`	`Multiset` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `ndinter`	—	`le_iff_subset` `Nodup.ndinter` `ndinter_subset_right`
`ndinter_subset_left` 📖	mathematical	—	`Multiset` `instHasSubset` `ndinter`	—	`subset_of_le` `ndinter_le_left`
`ndinter_subset_right` 📖	mathematical	—	`Multiset` `instHasSubset` `ndinter`	—	`le_ndinter` `le_rfl`
`ndunion_eq_union` 📖	mathematical	`Nodup`	`ndunion` `Multiset` `instUnion`	—	`le_antisymm` `ndunion_le_union` `union_le` `le_ndunion_left` `le_ndunion_right`
`ndunion_le` 📖	mathematical	—	`Multiset` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `ndunion` `instHasSubset`	—	`induction_on` `zero_ndunion` `cons_ndunion`
`ndunion_le_add` 📖	mathematical	—	`Multiset` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `ndunion` `instAdd`	—	`Quot.induction_on₂` `List.union_sublist_append`
`ndunion_le_union` 📖	mathematical	—	`Multiset` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `ndunion` `instUnion`	—	`ndunion_le` `subset_of_le` `le_union_left` `le_union_right`
`subset_ndunion_left` 📖	mathematical	—	`Multiset` `instHasSubset` `ndunion`	—	`mem_ndunion`
`subset_ndunion_right` 📖	mathematical	—	`Multiset` `instHasSubset` `ndunion`	—	`subset_of_le` `le_ndunion_right`
`zero_ndinter` 📖	mathematical	—	`ndinter` `Multiset` `instZero`	—	—
`zero_ndunion` 📖	mathematical	—	`ndunion` `Multiset` `instZero`	—	—

Multiset.Disjoint

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ndinter_eq_zero` 📖	mathematical	`Disjoint` `Multiset` `Multiset.instPartialOrder` `Multiset.instOrderBot`	`Multiset.ndinter` `Multiset.instZero`	—	`Multiset.ndinter_eq_zero_iff_disjoint`
`ndunion_eq` 📖	mathematical	`Disjoint` `Multiset` `Multiset.instPartialOrder` `Multiset.instOrderBot`	`Multiset.ndunion` `Multiset.instAdd` `Multiset.dedup`	—	`Quot.induction_on₂` `List.Disjoint.union_eq`

Multiset.Nodup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`inter` 📖	mathematical	`Multiset.Nodup`	`Multiset` `Multiset.instInter`	—	`Multiset.ndinter_eq_inter` `filter`
`ndinsert` 📖	mathematical	`Multiset.Nodup`	`Multiset.ndinsert`	—	`List.Nodup.insert`
`ndinter` 📖	mathematical	`Multiset.Nodup`	`Multiset.ndinter`	—	`filter`
`ndunion` 📖	mathematical	`Multiset.Nodup`	`Multiset.ndunion`	—	`Quot.induction_on₂` `List.Nodup.union`

Multiset.Subset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ndinter_eq_left` 📖	mathematical	`Multiset` `Multiset.instHasSubset`	`Multiset.ndinter`	—	`Quot.induction_on₂` `Multiset.quot_mk_to_coe''` `Multiset.coe_ndinter` `List.Subset.inter_eq_left`
`ndunion_eq_right` 📖	mathematical	`Multiset` `Multiset.instHasSubset`	`Multiset.ndunion`	—	`Quot.induction_on₂` `List.Subset.union_eq_right`

---

← Back to Index