Filter

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

Statistics

Metric	Count
Definitions `filter`, `filterMap`, `mapEmbedding`	3
Theorems `erase_eq_filter`, `filter`, `filterMap`, `mem_erase_iff`, `notMem_erase`, `card_filter_le_iff`, `countP_eq_card_filter`, `countP_eq_countP_filter_add`, `countP_filter`, `countP_map`, `count_eq_card_filter_eq`, `count_filter`, `count_filter_of_neg`, `count_filter_of_pos`, `count_map`, `count_map_eq_count`, `count_map_eq_count'`, `filterMap_add`, `filterMap_coe`, `filterMap_cons`, `filterMap_cons_none`, `filterMap_cons_some`, `filterMap_eq_filter`, `filterMap_eq_map`, `filterMap_filter`, `filterMap_filterMap`, `filterMap_le_filterMap`, `filterMap_map`, `filterMap_some`, `filterMap_zero`, `filter_add`, `filter_add_filter`, `filter_add_not`, `filter_attach`, `filter_attach'`, `filter_coe`, `filter_comm`, `filter_congr`, `filter_cons`, `filter_cons_of_neg`, `filter_cons_of_pos`, `filter_eq`, `filter_eq'`, `filter_eq_nil`, `filter_eq_self`, `filter_false`, `filter_filter`, `filter_filterMap`, `filter_le`, `filter_le_filter`, `filter_map`, `filter_singleton`, `filter_sub`, `filter_subset`, `filter_true`, `filter_zero`, `le_filter`, `mapEmbedding_apply`, `map_count_True_eq_filter_card`, `map_filter'`, `map_filterMap`, `map_filterMap_of_inv`, `map_filter_eq_filterMap`, `map_le_map_iff`, `mem_filter`, `mem_filterMap`, `mem_filter_of_mem`, `mem_of_mem_filter`, `monotone_filter_left`, `monotone_filter_right`, `of_mem_filter`, `sub_filter_eq_filter_not`	72
Total	75

Multiset

Definitions

Name	Category	Theorems
`filter` 📖	CompOp	81 math math: `filter_eq_self`, `Nat.Partition.ofMultiset_parts`, `filter_le_filter`, `filter_nsmul`, `card_filter_le_iff`, `BoxIntegral.TaggedPrepartition.filter_boxes_val`, `Ico_filter_lt_of_le_left`, `filter_cons`, `filter_singleton`, `toFinset_filter`, `filter_subset`, `PMF.toMeasure_ofMultiset_apply`, `count_filter_of_pos`, `filterMap_eq_filter`, `Ico_filter_le_of_le_left`, `bind_filter`, `Ico_filter_le_of_right_le`, `count_eq_card_filter_eq`, `filter_union`, `filter_add_filter`, `Ico_filter_le_left`, `Ico_filter_lt`, `nsmul_count`, `prod_filter_mul_prod_filter_not`, `filter_true`, `filter_eq_nil`, `Nodup.erase_eq_filter`, `multinomial_filter_ne`, `monotone_filter_right`, `filter_filter`, `PMF.toOuterMeasure_ofMultiset_apply`, `count_filter_of_neg`, `map_count_True_eq_filter_card`, `sum_filter_add_sum_filter_not`, `Ico_filter_lt_of_right_le`, `filter_add_not`, `filter_eq`, `countP_map`, `filter_le`, `filter_attach`, `filter_inter`, `Polynomial.filter_roots_map_range_eq_map_roots`, `filter_join`, `count_map`, `Ico_filter_lt_of_le_right`, `Ico_filter_le`, `pow_count`, `map_filter_eq_filterMap`, `monotone_filter_left`, `Finset.filter_val`, `Nat.Partition.ofSums_parts`, `filter_map`, `count_filter`, `filter_bind`, `filter_add`, `filter_sub`, `Finsupp.supportedEquivFinsupp_apply_support_val`, `filter_eq'`, `filter_cons_of_pos`, `filter_coe`, `Equiv.Perm.filter_parts_partition_eq_cycleType`, `mem_filter`, `map_filter'`, `filterMap_filter`, `filter_false`, `filter_eq_bind`, `filter_congr`, `filter_zero`, `sub_filter_eq_filter_not`, `Ico_filter_le_of_left_le`, `countP_eq_card_filter`, `filter_cons_of_neg`, `countP_eq_countP_filter_add`, `Nat.filter_multiset_Ico_card_eq_of_periodic`, `Nodup.filter`, `countP_filter`, `le_filter`, `filter_filterMap`, `filter_attach'`, `filter_comm`, `mem_filter_of_mem`
`filterMap` 📖	CompOp	24 math math: `filterMap_coe`, `bind_filterMap`, `filterMap_eq_map`, `filterMap_eq_filter`, `filterMap_map`, `map_filterMap`, `Finset.filterMap_val`, `filterMap_le_filterMap`, `map_filterMap_of_inv`, `filterMap_filterMap`, `filterMap_some`, `filterMap_zero`, `filterMap_eq_bind`, `mem_filterMap`, `filterMap_add`, `map_filter_eq_filterMap`, `Nodup.filterMap`, `filterMap_cons_some`, `filterMap_cons`, `filterMap_bind`, `filterMap_filter`, `filter_filterMap`, `filterMap_cons_none`, `filterMap_join`
`mapEmbedding` 📖	CompOp	1 math math: `mapEmbedding_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_filter_le_iff` 📖	mathematical	—	`card` `filter` `Multiset` `instMembership`	—	`LE.le.trans` `card_le_card` `monotone_filter_left` `LT.lt.not_ge` `filter_eq_self` `Mathlib.Tactic.Push.not_and_eq` `Mathlib.Tactic.Contrapose.contrapose₁` `Mathlib.Tactic.Push.not_forall_eq` `filter_le` `mem_filter`
`countP_eq_card_filter` 📖	mathematical	—	`countP` `card` `filter`	—	—
`countP_eq_countP_filter_add` 📖	mathematical	—	`countP` `filter`	—	`countP_congr`
`countP_filter` 📖	mathematical	—	`countP` `filter`	—	`countP_eq_card_filter` `filter_filter`
`countP_map` 📖	mathematical	—	`countP` `map` `card` `filter`	—	`induction_on` `map_zero` `countP_zero` `filter_zero` `card_zero` `map_cons` `countP_cons` `filter_cons` `card_add` `card_singleton`
`count_eq_card_filter_eq` 📖	mathematical	—	`count` `card` `filter`	—	`count.eq_1` `countP_eq_card_filter`
`count_filter` 📖	mathematical	—	`count` `filter`	—	`count_filter_of_pos` `count_filter_of_neg`
`count_filter_of_neg` 📖	mathematical	—	`count` `filter`	—	`count_eq_zero_of_notMem`
`count_filter_of_pos` 📖	mathematical	—	`count` `filter`	—	`coe_count`
`count_map` 📖	mathematical	—	`count` `map` `card` `filter`	—	`countP_map`
`count_map_eq_count` 📖	mathematical	`Set.InjOn` `setOf` `Multiset` `instMembership`	`count` `map`	—	`eq_replicate_card` `mem_filter` `filter_congr` `count_replicate` `card_replicate` `count.eq_1` `countP_map` `count_filter_of_pos`
`count_map_eq_count'` 📖	mathematical	—	`count` `map`	—	`count_map_eq_count` `Function.Injective.injOn` `count_eq_zero_of_notMem` `count_eq_zero` `mem_map`
`filterMap_add` 📖	mathematical	—	`filterMap` `Multiset` `instAdd`	—	—
`filterMap_coe` 📖	mathematical	—	`filterMap` `ofList`	—	—
`filterMap_cons` 📖	mathematical	—	`filterMap` `cons` `Multiset` `instAdd` `instSingleton` `instZero`	—	`filterMap_cons_none` `zero_add` `filterMap_cons_some`
`filterMap_cons_none` 📖	mathematical	—	`filterMap` `cons`	—	—
`filterMap_cons_some` 📖	mathematical	—	`filterMap` `cons`	—	—
`filterMap_eq_filter` 📖	mathematical	—	`filterMap` `filter`	—	—
`filterMap_eq_map` 📖	mathematical	—	`filterMap` `map`	—	—
`filterMap_filter` 📖	mathematical	—	`filterMap` `filter`	—	—
`filterMap_filterMap` 📖	mathematical	—	`filterMap`	—	—
`filterMap_le_filterMap` 📖	mathematical	`Multiset` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`filterMap`	—	`leInductionOn`
`filterMap_map` 📖	mathematical	—	`filterMap` `map`	—	—
`filterMap_some` 📖	mathematical	—	`filterMap`	—	—
`filterMap_zero` 📖	mathematical	—	`filterMap` `Multiset` `instZero`	—	—
`filter_add` 📖	mathematical	—	`filter` `Multiset` `instAdd`	—	—
`filter_add_filter` 📖	mathematical	—	`Multiset` `instAdd` `filter`	—	`induction_on` `filter_cons_of_pos` `add_cons` `cons_add` `filter_cons_of_neg`
`filter_add_not` 📖	mathematical	—	`Multiset` `instAdd` `filter`	—	`filter_add_filter` `filter_eq_self` `filter_eq_nil` `add_zero`
`filter_attach` 📖	mathematical	—	`filter` `Multiset` `instMembership` `attach` `map` `Subtype.map` `mem_of_mem_filter`	—	`mem_of_mem_filter` `List.mem_of_mem_filter` `List.filter_attach`
`filter_attach'` 📖	mathematical	—	`filter` `Multiset` `instMembership` `attach` `map` `decidableMem` `Subtype.map` `mem_of_mem_filter`	—	`map_injective` `Subtype.val_injective` `mem_of_mem_filter` `map_filter'` `filter_congr` `filter.congr_simp` `attach_map_val` `map_congr` `map_map`
`filter_coe` 📖	mathematical	—	`filter` `ofList`	—	—
`filter_comm` 📖	mathematical	—	`filter`	—	`filter_filter` `filter_congr`
`filter_congr` 📖	mathematical	—	`filter`	—	—
`filter_cons` 📖	mathematical	—	`filter` `cons` `Multiset` `instAdd` `instSingleton` `instZero`	—	`filter_cons_of_pos` `singleton_add` `filter_cons_of_neg` `zero_add`
`filter_cons_of_neg` 📖	mathematical	—	`filter` `cons`	—	—
`filter_cons_of_pos` 📖	mathematical	—	`filter` `cons`	—	—
`filter_eq` 📖	mathematical	—	`filter` `replicate` `count`	—	`filter_congr`
`filter_eq'` 📖	mathematical	—	`filter` `replicate` `count`	—	`coe_count` `coe_replicate`
`filter_eq_nil` 📖	mathematical	—	`filter` `Multiset` `instZero`	—	—
`filter_eq_self` 📖	mathematical	—	`filter`	—	—
`filter_false` 📖	mathematical	—	`filter` `Multiset` `instZero`	—	—
`filter_filter` 📖	mathematical	—	`filter`	—	—
`filter_filterMap` 📖	mathematical	—	`filter` `filterMap`	—	—
`filter_le` 📖	mathematical	—	`Multiset` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `filter`	—	—
`filter_le_filter` 📖	mathematical	`Multiset` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`filter`	—	`leInductionOn`
`filter_map` 📖	mathematical	—	`filter` `map`	—	`map_congr` `filter_congr`
`filter_singleton` 📖	mathematical	—	`filter` `Multiset` `instSingleton` `instEmptyCollection`	—	`filter_cons` `add_zero`
`filter_sub` 📖	mathematical	—	`filter` `Multiset` `instSub`	—	`induction_on` `filter.congr_simp` `sub_zero` `sub_cons` `filter_cons_of_pos` `cons_inj_right` `cons_erase` `mem_filter_of_mem` `erase_of_notMem` `mem_of_mem_filter` `filter_cons_of_neg`
`filter_subset` 📖	mathematical	—	`Multiset` `instHasSubset` `filter`	—	`subset_of_le` `filter_le`
`filter_true` 📖	mathematical	—	`filter`	—	—
`filter_zero` 📖	mathematical	—	`filter` `Multiset` `instZero`	—	—
`le_filter` 📖	mathematical	—	`Multiset` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `filter`	—	`le_trans` `filter_le` `of_mem_filter` `mem_of_le` `filter_le_filter` `filter_eq_self`
`mapEmbedding_apply` 📖	mathematical	—	`DFunLike.coe` `RelEmbedding` `Multiset` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `RelEmbedding.instFunLike` `mapEmbedding` `map` `Function.Embedding` `Function.instFunLikeEmbedding`	—	—
`map_count_True_eq_filter_card` 📖	mathematical	—	`count` `LinearOrder.toDecidableEq` `Prop.linearOrder` `map` `card` `filter`	—	`count_eq_card_filter_eq` `filter_map` `map_congr` `filter.congr_simp` `card_map`
`map_filter'` 📖	mathematical	—	`map` `filter`	—	`filter_map` `map_congr` `filter_congr`
`map_filterMap` 📖	mathematical	—	`map` `filterMap`	—	—
`map_filterMap_of_inv` 📖	mathematical	—	`map` `filterMap`	—	—
`map_filter_eq_filterMap` 📖	mathematical	—	`map` `filter` `filterMap`	—	`induction` `map_congr` `filter_cons` `map_add` `filterMap_cons`
`map_le_map_iff` 📖	mathematical	—	`Multiset` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `map`	—	`le_iff_count` `count_map_eq_count'` `map_le_map`
`mem_filter` 📖	mathematical	—	`Multiset` `instMembership` `filter`	—	—
`mem_filterMap` 📖	mathematical	—	`Multiset` `instMembership` `filterMap`	—	—
`mem_filter_of_mem` 📖	mathematical	`Multiset` `instMembership`	`filter`	—	`mem_filter`
`mem_of_mem_filter` 📖	—	`Multiset` `instMembership` `filter`	—	—	`mem_filter`
`monotone_filter_left` 📖	mathematical	—	`Monotone` `Multiset` `PartialOrder.toPreorder` `instPartialOrder` `filter`	—	`filter_le_filter`
`monotone_filter_right` 📖	mathematical	—	`Multiset` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `filter`	—	`List.monotone_filter_right`
`of_mem_filter` 📖	—	`Multiset` `instMembership` `filter`	—	—	`mem_filter`
`sub_filter_eq_filter_not` 📖	mathematical	—	`Multiset` `instSub` `filter`	—	`ext'` `count_sub` `count_filter_of_pos` `count_eq_zero_of_notMem`

Multiset.Nodup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`erase_eq_filter` 📖	mathematical	`Multiset.Nodup`	`Multiset.erase` `Multiset.filter`	—	`Quot.induction_on`
`filter` 📖	mathematical	`Multiset.Nodup`	`Multiset.filter`	—	`Quot.induction_on` `List.Nodup.filter`
`filterMap` 📖	mathematical	`Multiset.Nodup`	`Multiset.filterMap`	—	`Quot.induction_on` `List.Nodup.filterMap`
`mem_erase_iff` 📖	mathematical	`Multiset.Nodup`	`Multiset` `Multiset.instMembership` `Multiset.erase`	—	`erase_eq_filter` `Multiset.mem_filter`
`notMem_erase` 📖	mathematical	`Multiset.Nodup`	`Multiset` `Multiset.instMembership` `Multiset.erase`	—	`mem_erase_iff`

---

← Back to Index