UnionInter

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

Statistics

Metric	Count
Definitions `instDistribLattice`, `instInter`, `instLattice`, `instUnion`, `inter`, `union`	6
Theorems `notMem_of_mem_left_multiset`, `notMem_of_mem_right_multiset`, `add_iff`, `inter_left`, `inter_right`, `add_eq_union_iff_disjoint`, `add_eq_union_left_of_le`, `add_eq_union_right_of_le`, `add_inter_distrib`, `add_union_distrib`, `coe_disjoint`, `coe_inter`, `cons_inter_distrib`, `cons_inter_of_neg`, `cons_inter_of_pos`, `cons_union_distrib`, `count_inter`, `count_union`, `disjoint_add_left`, `disjoint_add_right`, `disjoint_cons_left`, `disjoint_cons_right`, `disjoint_iff_ne`, `disjoint_left`, `disjoint_map_map`, `disjoint_of_nodup_add`, `disjoint_of_subset_left`, `disjoint_of_subset_right`, `disjoint_right`, `disjoint_singleton`, `disjoint_union_left`, `disjoint_union_right`, `eq_union_left`, `eq_union_right`, `filter_inter`, `filter_union`, `inf_eq_inter`, `inter_add_distrib`, `inter_add_sub_of_add_eq_add`, `inter_comm`, `inter_eq_zero_iff_disjoint`, `inter_le_left`, `inter_le_right`, `inter_replicate`, `inter_zero`, `le_inter`, `le_inter_iff`, `le_union_left`, `le_union_right`, `map_set_pairwise`, `map_union`, `mem_inter`, `mem_union`, `nodup_add`, `nodup_union`, `replicate_inter`, `singleton_disjoint`, `sub_add_inter`, `sub_inter`, `sup_eq_union`, `union_add_distrib`, `union_add_inter`, `union_comm`, `union_def`, `union_le`, `union_le_add`, `union_le_iff`, `union_le_union_left`, `union_le_union_right`, `union_zero`, `zero_disjoint`, `zero_inter`, `zero_union`	73
Total	79

Disjoint

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`notMem_of_mem_left_multiset` 📖	—	`Disjoint` `Multiset` `Multiset.instPartialOrder` `Multiset.instOrderBot` `Multiset.instMembership`	—	—	`Multiset.disjoint_left`
`notMem_of_mem_right_multiset` 📖	—	`Disjoint` `Multiset` `Multiset.instPartialOrder` `Multiset.instOrderBot` `Multiset.instMembership`	—	—	`Multiset.disjoint_right`

Multiset

Definitions

Name	Category	Theorems
`instDistribLattice` 📖	CompOp	—
`instInter` 📖	CompOp	39 math math: `coe_inter`, `add_inter_distrib`, `fold_union_inter`, `inter_add_sub_of_add_eq_add`, `Nodup.inter`, `union_add_inter`, `toFinsupp_inter`, `Nodup.inter_left`, `Nodup.inter_right`, `le_inter`, `cons_inter_of_pos`, `replicate_inter`, `le_inter_iff`, `Ico_inter_Ico`, `filter_inter`, `DFinsupp.toMultiset_inf`, `inter_zero`, `count_inter`, `inter_le_ndinter`, `Ico_inter_Ico_of_le`, `inf_eq_inter`, `inter_le_right`, `zero_inter`, `inter_le_left`, `ndinter_eq_inter`, `sub_add_inter`, `toFinset_inter`, `sub_inter`, `toDFinsupp_inter`, `sup_eq_prod_inf_factors`, `cons_inter_of_neg`, `Finset.inter_val`, `cons_inter_distrib`, `inter_comm`, `Finsupp.toMultiset_inf`, `inter_replicate`, `inter_eq_zero_iff_disjoint`, `inter_add_distrib`, `mem_inter`
`instLattice` 📖	CompOp	15 math math: `sup_eq_union`, `MvPolynomial.degrees_def`, `sup_powerset_len`, `finset_sum_eq_sup_iff_disjoint`, `card_uIcc`, `uIcc_eq`, `nodup_sup_iff`, `MvPolynomial.degrees_sum_le`, `map_finset_sup`, `mem_sup`, `MvPolynomial.degrees_add_le`, `count_finset_sup`, `inf_eq_inter`, `Finset.sup_toFinset`, `Associates.FactorSet.sup_add_inf_eq_add`
`instUnion` 📖	CompOp	44 math math: `ndunion_le_union`, `DFinsupp.toMultiset_sup`, `sup_eq_union`, `union_le_iff`, `range_add_eq_union`, `fold_union_inter`, `ndunion_eq_union`, `mem_union`, `add_eq_union_iff_disjoint`, `disjoint_union_left`, `filter_union`, `toFinsupp_union`, `union_le_union_left`, `cons_union_distrib`, `le_union_right`, `union_add_inter`, `count_union`, `MvPolynomial.degrees_sub_le`, `le_union_left`, `union_le_union_right`, `lcm_union`, `nodup_union`, `union_le`, `map_union`, `toFinset_union`, `disjoint_union_right`, `eq_union_right`, `union_le_add`, `inf_union`, `Finset.union_val`, `add_union_distrib`, `zero_union`, `union_comm`, `gcd_union`, `sup_union`, `union_add_distrib`, `toDFinsupp_union`, `eq_union_left`, `union_zero`, `Finsupp.toMultiset_sup`, `add_eq_union_left_of_le`, `MvPolynomial.degrees_add_of_disjoint`, `add_eq_union_right_of_le`, `union_def`
`inter` 📖	CompOp	—
`union` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_eq_union_iff_disjoint` 📖	mathematical	—	`Multiset` `instAdd` `instUnion` `Disjoint` `instPartialOrder` `instOrderBot`	—	`count_add` `count_union` `count_inter`
`add_eq_union_left_of_le` 📖	mathematical	`Multiset` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`instAdd` `instUnion` `Disjoint` `instOrderBot`	—	`add_eq_union_iff_disjoint` `LE.le.antisymm` `le_of_add_le_add_left` `Eq.trans_le` `union_le_add`
`add_eq_union_right_of_le` 📖	mathematical	`Multiset` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`instAdd` `instUnion` `Disjoint` `instOrderBot`	—	`add_eq_union_left_of_le`
`add_inter_distrib` 📖	mathematical	—	`Multiset` `instAdd` `instInter`	—	`add_comm` `inter_add_distrib`
`add_union_distrib` 📖	mathematical	—	`Multiset` `instAdd` `instUnion`	—	`add_comm` `union_add_distrib`
`coe_disjoint` 📖	mathematical	—	`Disjoint` `Multiset` `instPartialOrder` `instOrderBot` `ofList`	—	`disjoint_left`
`coe_inter` 📖	mathematical	—	`Multiset` `instInter` `ofList`	—	`ext'` `count_inter` `coe_count` `List.count_bagInter`
`cons_inter_distrib` 📖	mathematical	—	`cons` `Multiset` `instInter`	—	`cons_inter_of_pos` `erase_cons_head`
`cons_inter_of_neg` 📖	mathematical	`Multiset` `instMembership`	`instInter` `cons`	—	`List.cons_bagInter_of_neg`
`cons_inter_of_pos` 📖	mathematical	`Multiset` `instMembership`	`instInter` `cons` `erase`	—	`List.cons_bagInter_of_pos`
`cons_union_distrib` 📖	mathematical	—	`cons` `Multiset` `instUnion`	—	`add_union_distrib`
`count_inter` 📖	mathematical	—	`count` `Multiset` `instInter`	—	`count_add` `sub_add_inter` `count_sub`
`count_union` 📖	mathematical	—	`count` `Multiset` `instUnion`	—	`count_add` `count_sub`
`disjoint_add_left` 📖	mathematical	—	`Disjoint` `Multiset` `instPartialOrder` `instOrderBot` `instAdd`	—	—
`disjoint_add_right` 📖	mathematical	—	`Disjoint` `Multiset` `instPartialOrder` `instOrderBot` `instAdd`	—	`disjoint_comm` `disjoint_add_left`
`disjoint_cons_left` 📖	mathematical	—	`Disjoint` `Multiset` `instPartialOrder` `instOrderBot` `cons` `instMembership`	—	`disjoint_add_left` `singleton_disjoint`
`disjoint_cons_right` 📖	mathematical	—	`Disjoint` `Multiset` `instPartialOrder` `instOrderBot` `cons` `instMembership`	—	`disjoint_comm` `disjoint_cons_left`
`disjoint_iff_ne` 📖	mathematical	—	`Disjoint` `Multiset` `instPartialOrder` `instOrderBot`	—	—
`disjoint_left` 📖	mathematical	—	`Disjoint` `Multiset` `instPartialOrder` `instOrderBot` `instMembership`	—	`singleton_le` `le_bot_iff` `bot_eq_zero` `eq_zero_iff_forall_notMem` `subset_of_le`
`disjoint_map_map` 📖	mathematical	—	`Disjoint` `Multiset` `instPartialOrder` `instOrderBot` `map`	—	—
`disjoint_of_nodup_add` 📖	mathematical	`Nodup` `Multiset` `instAdd`	`Disjoint` `instPartialOrder` `instOrderBot`	—	`nodup_add`
`disjoint_of_subset_left` 📖	—	`Multiset` `instHasSubset` `Disjoint` `instPartialOrder` `instOrderBot`	—	—	`disjoint_left`
`disjoint_of_subset_right` 📖	—	`Multiset` `instHasSubset` `Disjoint` `instPartialOrder` `instOrderBot`	—	—	`Disjoint.symm` `disjoint_of_subset_left`
`disjoint_right` 📖	mathematical	—	`Disjoint` `Multiset` `instPartialOrder` `instOrderBot` `instMembership`	—	`disjoint_comm` `disjoint_left`
`disjoint_singleton` 📖	mathematical	—	`Disjoint` `Multiset` `instPartialOrder` `instOrderBot` `instSingleton` `instMembership`	—	`disjoint_comm` `singleton_disjoint`
`disjoint_union_left` 📖	mathematical	—	`Disjoint` `Multiset` `instPartialOrder` `instOrderBot` `instUnion`	—	`disjoint_sup_left`
`disjoint_union_right` 📖	mathematical	—	`Disjoint` `Multiset` `instPartialOrder` `instOrderBot` `instUnion`	—	`disjoint_sup_right`
`eq_union_left` 📖	mathematical	`Multiset` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`instUnion`	—	`sub_add_cancel`
`eq_union_right` 📖	mathematical	`Multiset` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`instUnion`	—	`union_comm` `eq_union_left`
`filter_inter` 📖	mathematical	—	`filter` `Multiset` `instInter`	—	`le_antisymm` `le_inter` `filter_le_filter` `inter_le_left` `inter_le_right` `le_filter` `inf_le_inf` `filter_le` `of_mem_filter` `mem_of_le`
`filter_union` 📖	mathematical	—	`filter` `Multiset` `instUnion`	—	`filter_add` `filter_sub`
`inf_eq_inter` 📖	mathematical	—	`Multiset` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `instLattice` `instInter`	—	—
`inter_add_distrib` 📖	mathematical	—	`Multiset` `instAdd` `instInter`	—	`lt_iff_cons_le` `Ne.lt_of_le` `le_inter` `add_le_add_right` `inter_le_left` `inter_le_right` `LT.lt.not_ge` `lt_cons_self` `le_of_add_le_add_right` `LE.le.trans` `cons_add`
`inter_add_sub_of_add_eq_add` 📖	mathematical	`Multiset` `instAdd`	`instInter` `instSub`	—	`ext'` `count_add` `count_inter` `count_sub` `ext`
`inter_comm` 📖	mathematical	—	`Multiset` `instInter`	—	`inf_comm`
`inter_eq_zero_iff_disjoint` 📖	mathematical	—	`Multiset` `instInter` `instZero` `Disjoint` `instPartialOrder` `instOrderBot`	—	`subset_zero`
`inter_le_left` 📖	mathematical	—	`Multiset` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `instInter`	—	`List.bagInter_sublist_left`
`inter_le_right` 📖	mathematical	—	`Multiset` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `instInter`	—	`induction_on` `zero_le` `zero_inter` `cons_inter_of_pos` `cons_erase` `cons_le_cons` `cons_inter_of_neg`
`inter_replicate` 📖	mathematical	—	`Multiset` `instInter` `replicate` `count`	—	`inter_comm` `replicate_inter` `min_comm`
`inter_zero` 📖	mathematical	—	`Multiset` `instInter` `instZero`	—	`List.bagInter_nil`
`le_inter` 📖	mathematical	`Multiset` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`instInter`	—	`induction_on` `zero_inter` `cons_inter_of_pos` `erase_le_iff_le_cons` `erase_le_erase` `cons_inter_of_neg` `le_cons_of_notMem` `mem_of_le`
`le_inter_iff` 📖	mathematical	—	`Multiset` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `instInter`	—	`le_inf_iff`
`le_union_left` 📖	mathematical	—	`Multiset` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `instUnion`	—	`le_sub_add`
`le_union_right` 📖	mathematical	—	`Multiset` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `instUnion`	—	`le_add_left`
`map_set_pairwise` 📖	mathematical	`Set.Pairwise` `setOf` `Multiset` `instMembership`	`map`	—	`mem_map`
`map_union` 📖	mathematical	—	`map` `Multiset` `instUnion`	—	`List.map_diff`
`mem_inter` 📖	mathematical	—	`Multiset` `instMembership` `instInter`	—	`mem_of_le` `inter_le_left` `inter_le_right` `cons_erase` `cons_inter_of_pos` `mem_cons_self`
`mem_union` 📖	mathematical	—	`Multiset` `instMembership` `instUnion`	—	`mem_of_le` `sub_le_self` `mem_add` `le_union_left` `le_union_right`
`nodup_add` 📖	mathematical	—	`Nodup` `Multiset` `instAdd` `Disjoint` `instPartialOrder` `instOrderBot`	—	—
`nodup_union` 📖	mathematical	—	`Nodup` `Multiset` `instUnion`	—	`nodup_of_le` `le_union_left` `le_union_right` `nodup_iff_count_le_one` `count_union` `max_le`
`replicate_inter` 📖	mathematical	—	`Multiset` `instInter` `replicate` `count`	—	`ext'` `count_inter` `count_replicate` `count.congr_simp`
`singleton_disjoint` 📖	mathematical	—	`Disjoint` `Multiset` `instPartialOrder` `instOrderBot` `instSingleton` `instMembership`	—	—
`sub_add_inter` 📖	mathematical	—	`Multiset` `instAdd` `instSub` `instInter`	—	`inter_comm` `induction_on` `sub_zero` `zero_inter` `add_zero` `cons_inter_of_pos` `sub_cons` `add_cons` `cons_erase` `cons_inter_of_neg` `erase_of_notMem`
`sub_inter` 📖	mathematical	—	`Multiset` `instSub` `instInter`	—	`eq_sub_of_add_eq` `sub_add_inter`
`sup_eq_union` 📖	mathematical	—	`Multiset` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `instLattice` `instUnion`	—	—
`union_add_distrib` 📖	mathematical	—	`Multiset` `instAdd` `instUnion`	—	`add_assoc` `add_comm` `sub_add_eq_sub_sub` `add_sub_cancel_right`
`union_add_inter` 📖	mathematical	—	`Multiset` `instAdd` `instUnion` `instInter`	—	`le_antisymm` `union_add_distrib` `union_le` `add_le_add_left` `inter_le_right` `add_comm` `add_le_add_right` `inter_le_left` `add_inter_distrib` `le_inter` `le_union_right` `le_union_left`
`union_comm` 📖	mathematical	—	`Multiset` `instUnion`	—	`sup_comm`
`union_def` 📖	mathematical	—	`Multiset` `instUnion` `instAdd` `instSub`	—	—
`union_le` 📖	mathematical	`Multiset` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`instUnion`	—	`eq_union_left` `union_le_union_right`
`union_le_add` 📖	mathematical	—	`Multiset` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `instUnion` `instAdd`	—	`union_le` `le_add_right` `le_add_left`
`union_le_iff` 📖	mathematical	—	`Multiset` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `instUnion`	—	`sup_le_iff`
`union_le_union_left` 📖	mathematical	`Multiset` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`instUnion`	—	`sup_le_sup_left`
`union_le_union_right` 📖	mathematical	`Multiset` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`instUnion`	—	`add_le_add_right` `sub_le_sub_right`
`union_zero` 📖	mathematical	—	`Multiset` `instUnion` `instZero`	—	`sub_zero` `add_zero`
`zero_disjoint` 📖	mathematical	—	`Disjoint` `Multiset` `instPartialOrder` `instOrderBot` `instZero`	—	`disjoint_bot_left`
`zero_inter` 📖	mathematical	—	`Multiset` `instInter` `instZero`	—	`List.nil_bagInter`
`zero_union` 📖	mathematical	—	`Multiset` `instUnion` `instZero`	—	`zero_sub` `zero_add`

Multiset.Nodup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_iff` 📖	mathematical	`Multiset.Nodup`	`Multiset` `Multiset.instAdd` `Disjoint` `Multiset.instPartialOrder` `Multiset.instOrderBot`	—	—
`inter_left` 📖	mathematical	`Multiset.Nodup`	`Multiset` `Multiset.instInter`	—	`Multiset.nodup_of_le` `Multiset.inter_le_left`
`inter_right` 📖	mathematical	`Multiset.Nodup`	`Multiset` `Multiset.instInter`	—	`Multiset.nodup_of_le` `Multiset.inter_le_right`

---

← Back to Index