Union

📁 Source: Mathlib/Data/Finset/Union.lean

Statistics

Metric	Count
Definitions `biUnion`, `disjiUnion`	2
Theorems `biUnion`, `biUnion_biUnion`, `biUnion_congr`, `biUnion_empty`, `biUnion_filter_eq_of_maps_to`, `biUnion_image`, `biUnion_insert`, `biUnion_inter`, `biUnion_mono`, `biUnion_nonempty`, `biUnion_singleton`, `biUnion_singleton_eq_self`, `biUnion_subset`, `biUnion_subset_biUnion_of_subset_left`, `biUnion_subset_iff_forall_subset`, `biUnion_union`, `biUnion_val`, `bind_toFinset`, `coe_biUnion`, `coe_disjiUnion`, `disjiUnion_cons`, `disjiUnion_disjUnion`, `disjiUnion_disjiUnion`, `disjiUnion_empty`, `disjiUnion_eq_biUnion`, `disjiUnion_filter_eq`, `disjiUnion_filter_eq_of_maps_to`, `disjiUnion_map`, `disjiUnion_singleton`, `disjiUnion_singleton_eq_self`, `disjiUnion_val`, `disjoint_biUnion_left`, `disjoint_biUnion_right`, `disjoint_disjiUnion_left`, `disjoint_disjiUnion_right`, `erase_biUnion`, `filter_biUnion`, `filter_disjiUnion`, `fold_disjiUnion`, `image_biUnion`, `image_biUnion_filter_eq`, `inter_biUnion`, `map_disjiUnion`, `mem_biUnion`, `mem_disjiUnion`, `pairwiseDisjoint_disjUnion`, `pairwiseDisjoint_filter`, `sUnion_disjiUnion`, `singleton_biUnion`, `singleton_disjiUnion`, `subset_biUnion_of_mem`, `union_biUnion`	52
Total	54

Finset

Definitions

Name	Category	Theorems
`biUnion` 📖	CompOp	127 math math: `iSup_biUnion`, `prod_biUnion_of_pairwise_eq_one`, `Finsupp.support_finset_sum`, `MvPolynomial.support_sum`, `MvPolynomial.vars_sum_of_disjoint`, `set_biUnion_biUnion`, `biUnion_image_sdiff_left`, `product_biUnion`, `card_le_card_biUnion`, `Finpartition.combine_parts`, `biUnion_image_sdiff_right`, `Finpartition.equitabilise_aux`, `Rel.interedges_biUnion`, `IsPrimitiveRoot.nthRoots_one_eq_biUnion_primitiveRoots`, `Rel.interedges_eq_biUnion`, `erase_biUnion`, `biUnion_image_left`, `coe_biUnion`, `Tree.treesOfNumNodesEq_succ`, `Finpartition.card_parts_equitabilise_subset_le`, `biUnion_image`, `Finpartition.IsEquipartition.card_biUnion_offDiag_le'`, `Algebra.FormallyUnramified.finite_of_free_aux`, `Nonempty.biUnion`, `prod_biUnion`, `sum_biUnion_of_pairwise_eq_zero`, `inf_biUnion`, `biUnion_subset_iff_forall_subset`, `biUnion_val`, `Finpartition.IsEquipartition.card_biUnion_offDiag_le`, `disjiUnion_eq_biUnion`, `biUnion_nonempty`, `prod_indicator_biUnion_finset_sub_indicator`, `SkewMonoidAlgebra.support_sum`, `Algebra.adjoin_attach_biUnion`, `biUnion_mono`, `piAntidiag_insert`, `Nat.roughNumbersUpTo_eq_biUnion`, `Finpartition.IsEquipartition.card_interedges_sparsePairs_le`, `Submodule.span_attach_biUnion`, `product_eq_biUnion`, `all_card_le_biUnion_card_iff_existsInjective'`, `biUnion_slice`, `BoxIntegral.Prepartition.sum_biUnion_boxes`, `powerset_card_biUnion`, `Finpartition.bind_parts`, `MvPolynomial.vars_eq_support_biUnion_support`, `Equiv.Perm.support_noncommProd`, `singleton_biUnion`, `biUnion_filter_eq_of_maps_to`, `card_biUnion`, `Finsupp.support_sum`, `Rel.interedges_biUnion_left`, `SzemerediRegularity.biUnion_star_subset_nonuniformWitness`, `iInf_biUnion`, `biUnion_union`, `biUnion_empty`, `biUnion_op_vadd_finset`, `dens_biUnion_le`, `Rel.interedges_biUnion_right`, `card_le_card_biUnion_add_one`, `biUnion_subset_biUnion_of_subset_left`, `inclusion_exclusion_card_biUnion`, `sup_eq_biUnion`, `product_eq_biUnion_right`, `MvPolynomial.support_esymm'`, `Finpartition.biUnion_parts`, `Equiv.Perm.Basis.ofPermHom_support`, `SimpleGraph.unreduced_edges_subset`, `MvPolynomial.vars_prod`, `biUnion_singleton_eq_self`, `biUnion_insert`, `BoxIntegral.Prepartition.biUnion_boxes`, `subset_biUnion_of_mem`, `biUnion_image_sup_right`, `union_biUnion`, `Finpartition.IsEquipartition.sum_nonUniforms_lt`, `card_biUnion_le_of_intersecting`, `biUnion_inter`, `eraseNone_eq_biUnion`, `disjoint_biUnion_left`, `all_card_le_biUnion_card_iff_exists_injective`, `biUnion_image_inf_right`, `image_biUnion`, `biUnion_vadd_finset`, `MvPolynomial.vars_bind₁`, `inter_biUnion`, `biUnion_image_sup_left`, `biUnion_image_right`, `inclusion_exclusion_sum_biUnion`, `inf'_biUnion`, `Set.toFinset_iUnion`, `SupIndep.biUnion`, `card_biUnion_le_card_mul`, `card_le_card_biUnion_add_card_fiber`, `card_biUnion_le`, `dens_biUnion`, `biUnion_subset`, `MvPolynomial.support_esymm''`, `disjoint_biUnion_right`, `sum_biUnion`, `biUnion_biUnion`, `biUnion_congr`, `sigma_eq_biUnion`, `image_biUnion_filter_eq`, `finsuppAntidiag_insert`, `SimpleGraph.interedges_biUnion`, `biUnion_singleton`, `SimpleGraph.interedges_biUnion_left`, `sup_biUnion`, `biUnion_op_smul_finset`, `filter_biUnion`, `biUnion_smul_finset`, `SzemerediRegularity.card_biUnion_star_le_m_add_one_card_star_mul`, `Finpartition.biUnion_filter_atomise`, `biUnion_image_inf_left`, `DFinsupp.support_sum`, `Finsupp.support_sum_eq_biUnion`, `mem_biUnion`, `MvPolynomial.vars_sum_subset`, `pi_insert`, `set_biInter_biUnion`, `SimpleGraph.interedges_biUnion_right`, `Turing.PartrecToTM2.supports_biUnion`, `bind_toFinset`, `sup'_biUnion`, `Finpartition.IsEquipartition.card_interedges_sparsePairs_le'`
`disjiUnion` 📖	CompOp	30 math math: `disjiUnion_filter_eq`, `disjiUnion_singleton_eq_self`, `disjiUnion_filter_eq_of_maps_to`, `SimpleGraph.disjiUnion_supp_toFinset_eq_supp_toFinset`, `disjiUnion_eq_biUnion`, `List.fixedLengthDigits_succ_eq_disjiUnion`, `prod_disjiUnion`, `disjiUnion_disjUnion`, `card_disjiUnion`, `dens_disjiUnion`, `disjoint_disjiUnion_right`, `singleton_disjiUnion`, `mem_disjiUnion`, `fold_disjiUnion`, `disjiUnion_singleton`, `coe_disjiUnion`, `disjoint_disjiUnion_left`, `piAntidiag_cons`, `sUnion_disjiUnion`, `filter_disjiUnion`, `disjiUnion_empty`, `disjiUnion_map`, `powerset_card_disjiUnion`, `sum_disjiUnion`, `product_self_eq_disjiUnion_perm`, `map_disjiUnion`, `disjiUnion_cons`, `disjiUnion_Iic_disjointed`, `disjiUnion_val`, `disjiUnion_map_sigma_mk`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`biUnion_biUnion` 📖	mathematical	—	`biUnion`	—	—
`biUnion_congr` 📖	mathematical	—	`biUnion`	—	—
`biUnion_empty` 📖	mathematical	—	`biUnion` `Finset` `instEmptyCollection`	—	—
`biUnion_filter_eq_of_maps_to` 📖	mathematical	`Finset` `instMembership`	`biUnion` `filter`	—	—
`biUnion_image` 📖	mathematical	—	`image` `biUnion`	—	`induction_on` `biUnion_insert` `image_union`
`biUnion_insert` 📖	mathematical	—	`biUnion` `Finset` `instInsert` `instUnion`	—	`ext`
`biUnion_inter` 📖	mathematical	—	`Finset` `instInter` `biUnion`	—	—
`biUnion_mono` 📖	mathematical	`Finset` `instHasSubset`	`biUnion`	—	—
`biUnion_nonempty` 📖	mathematical	—	`Nonempty` `biUnion` `Finset` `instMembership`	—	`exists_swap`
`biUnion_singleton` 📖	mathematical	—	`biUnion` `Finset` `instSingleton` `image`	—	—
`biUnion_singleton_eq_self` 📖	mathematical	—	`biUnion` `Finset` `instSingleton`	—	—
`biUnion_subset` 📖	mathematical	—	`Finset` `instHasSubset` `biUnion`	—	—
`biUnion_subset_biUnion_of_subset_left` 📖	mathematical	`Finset` `instHasSubset`	`biUnion`	—	—
`biUnion_subset_iff_forall_subset` 📖	mathematical	—	`Finset` `instHasSubset` `biUnion`	—	—
`biUnion_union` 📖	mathematical	—	`biUnion` `Finset` `instUnion`	—	—
`biUnion_val` 📖	mathematical	—	`val` `biUnion` `Multiset.dedup` `Multiset.bind`	—	—
`bind_toFinset` 📖	mathematical	—	`Multiset.toFinset` `Multiset.bind` `biUnion`	—	`ext`
`coe_biUnion` 📖	mathematical	—	`SetLike.coe` `Finset` `instSetLike` `biUnion` `Set.iUnion` `Set` `Set.instMembership`	—	—
`coe_disjiUnion` 📖	mathematical	`Set.PairwiseDisjoint` `Finset` `partialOrder` `instOrderBot` `SetLike.coe` `instSetLike`	`disjiUnion` `Set.iUnion` `Set` `Set.instMembership`	—	—
`disjiUnion_cons` 📖	mathematical	`Finset` `instMembership` `Set.PairwiseDisjoint` `partialOrder` `instOrderBot` `SetLike.coe` `instSetLike` `cons`	`disjiUnion` `disjUnion` `mem_cons_of_mem` `Disjoint` `disjoint_left` `mem_disjiUnion` `mem_cons_self`	—	`eq_of_veq` `mem_cons_of_mem` `disjoint_left` `mem_disjiUnion` `mem_cons_self` `Multiset.cons_bind`
`disjiUnion_disjUnion` 📖	mathematical	`Disjoint` `Finset` `partialOrder` `instOrderBot` `Set.Pairwise` `SetLike.coe` `instSetLike` `Set.PairwiseDisjoint`	`disjiUnion` `disjUnion` `pairwiseDisjoint_disjUnion`	—	—
`disjiUnion_disjiUnion` 📖	mathematical	`Set.PairwiseDisjoint` `Finset` `partialOrder` `instOrderBot` `SetLike.coe` `instSetLike` `disjiUnion`	`instMembership` `attach` `mem_disjiUnion` `Subtype.prop` `Disjoint` `disjoint_left`	—	`eq_of_veq` `mem_disjiUnion` `Subtype.prop` `disjoint_left` `Multiset.bind_assoc` `Multiset.attach_bind_coe`
`disjiUnion_empty` 📖	mathematical	—	`disjiUnion` `Finset` `instEmptyCollection`	—	—
`disjiUnion_eq_biUnion` 📖	mathematical	`Set.PairwiseDisjoint` `Finset` `partialOrder` `instOrderBot` `SetLike.coe` `instSetLike`	`disjiUnion` `biUnion`	—	`eq_of_veq` `Multiset.Nodup.dedup` `nodup`
`disjiUnion_filter_eq` 📖	mathematical	—	`disjiUnion` `filter` `Finset` `instMembership` `decidableMem`	—	`ext`
`disjiUnion_filter_eq_of_maps_to` 📖	mathematical	`Finset` `instMembership`	`disjiUnion` `filter`	—	`disjiUnion_filter_eq`
`disjiUnion_map` 📖	mathematical	`Set.PairwiseDisjoint` `Finset` `partialOrder` `instOrderBot` `SetLike.coe` `instSetLike`	`map` `disjiUnion` `Set.Pairwise.mono'` `Disjoint` `Function.onFun` `disjoint_map`	—	`eq_of_veq` `Set.Pairwise.mono'` `disjoint_map` `Multiset.map_bind`
`disjiUnion_singleton` 📖	mathematical	—	`disjiUnion` `Finset` `instSingleton` `Function.onFun` `Disjoint` `partialOrder` `instOrderBot` `disjoint_singleton` `map`	—	`ext` `disjoint_singleton`
`disjiUnion_singleton_eq_self` 📖	mathematical	—	`disjiUnion` `Finset` `instSingleton`	—	—
`disjiUnion_val` 📖	mathematical	`Set.PairwiseDisjoint` `Finset` `partialOrder` `instOrderBot` `SetLike.coe` `instSetLike`	`val` `disjiUnion` `Multiset.bind`	—	—
`disjoint_biUnion_left` 📖	mathematical	—	`Disjoint` `Finset` `partialOrder` `instOrderBot` `biUnion`	—	`induction` `biUnion_insert`
`disjoint_biUnion_right` 📖	mathematical	—	`Disjoint` `Finset` `partialOrder` `instOrderBot` `biUnion`	—	`disjoint_biUnion_left`
`disjoint_disjiUnion_left` 📖	mathematical	`Set.PairwiseDisjoint` `Finset` `partialOrder` `instOrderBot` `SetLike.coe` `instSetLike`	`Disjoint` `disjiUnion`	—	`cons_induction` `instIsEmptyFalse` `mem_cons_of_mem` `disjoint_left` `mem_disjiUnion` `mem_cons_self` `disjiUnion_cons`
`disjoint_disjiUnion_right` 📖	mathematical	`Set.PairwiseDisjoint` `Finset` `partialOrder` `instOrderBot` `SetLike.coe` `instSetLike`	`Disjoint` `disjiUnion`	—	`disjoint_disjiUnion_left`
`erase_biUnion` 📖	mathematical	—	`erase` `biUnion`	—	—
`filter_biUnion` 📖	mathematical	—	`filter` `biUnion`	—	—
`filter_disjiUnion` 📖	mathematical	`Set.PairwiseDisjoint` `Finset` `partialOrder` `instOrderBot` `SetLike.coe` `instSetLike`	`filter` `disjiUnion` `pairwiseDisjoint_filter`	—	—
`fold_disjiUnion` 📖	mathematical	`Set.PairwiseDisjoint` `Finset` `partialOrder` `instOrderBot` `SetLike.coe` `instSetLike`	`fold` `disjiUnion`	—	`Multiset.map_bind` `Multiset.fold_bind`
`image_biUnion` 📖	mathematical	—	`biUnion` `image`	—	`induction_on` `image_insert` `biUnion_insert`
`image_biUnion_filter_eq` 📖	mathematical	—	`biUnion` `image` `filter`	—	`biUnion_filter_eq_of_maps_to` `mem_image_of_mem`
`inter_biUnion` 📖	mathematical	—	`Finset` `instInter` `biUnion`	—	—
`map_disjiUnion` 📖	mathematical	`Set.PairwiseDisjoint` `Finset` `partialOrder` `instOrderBot` `SetLike.coe` `instSetLike` `map`	`disjiUnion` `DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `mem_map_of_mem` `Function.Embedding.injective`	—	`eq_of_veq` `mem_map_of_mem` `Function.Embedding.injective` `Multiset.bind_map`
`mem_biUnion` 📖	mathematical	—	`Finset` `instMembership` `biUnion`	—	—
`mem_disjiUnion` 📖	mathematical	`Set.PairwiseDisjoint` `Finset` `partialOrder` `instOrderBot` `SetLike.coe` `instSetLike`	`instMembership` `disjiUnion`	—	—
`pairwiseDisjoint_disjUnion` 📖	mathematical	`Disjoint` `Finset` `partialOrder` `instOrderBot` `Set.Pairwise` `SetLike.coe` `instSetLike` `Set.PairwiseDisjoint`	`disjUnion`	—	`Disjoint.symm`
`pairwiseDisjoint_filter` 📖	mathematical	`Set.PairwiseDisjoint` `Finset` `partialOrder` `instOrderBot` `SetLike.coe` `instSetLike`	`filter`	—	`disjoint_filter_filter`
`sUnion_disjiUnion` 📖	mathematical	`Set.PairwiseDisjoint` `Finset` `Set` `partialOrder` `instOrderBot` `SetLike.coe` `instSetLike`	`Set.sUnion` `disjiUnion` `Set.iUnion` `instMembership`	—	`Set.ext` `coe_disjiUnion`
`singleton_biUnion` 📖	mathematical	—	`biUnion` `Finset` `instSingleton`	—	—
`singleton_disjiUnion` 📖	mathematical	`Set.PairwiseDisjoint` `Finset` `partialOrder` `instOrderBot` `SetLike.coe` `instSetLike` `instSingleton`	`disjiUnion`	—	`eq_of_veq` `Multiset.singleton_bind`
`subset_biUnion_of_mem` 📖	mathematical	`Finset` `instMembership`	`instHasSubset` `biUnion`	—	—
`union_biUnion` 📖	mathematical	—	`biUnion` `Finset` `instUnion`	—	—

Finset.Nonempty

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`biUnion` 📖	mathematical	`Finset.Nonempty`	`Finset.biUnion`	—	`Finset.biUnion_nonempty`

---

← Back to Index