Disjoint

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

Statistics

Metric	Count
Definitions `decidableDisjoint`, `disjUnion`	2
Theorems `forall_ne_finset`, `notMem_of_mem_left_finset`, `notMem_of_mem_right_finset`, `coe_disjUnion`, `disjUnion_comm`, `disjUnion_empty`, `disjUnion_inj_left`, `disjUnion_inj_right`, `disjUnion_singleton`, `disjUnion_val`, `disjoint_coe`, `disjoint_empty_left`, `disjoint_empty_right`, `disjoint_iff_ne`, `disjoint_insert_left`, `disjoint_insert_right`, `disjoint_left`, `disjoint_of_subset_left`, `disjoint_of_subset_right`, `disjoint_right`, `disjoint_self_iff_empty`, `disjoint_singleton`, `disjoint_singleton_left`, `disjoint_singleton_right`, `disjoint_val`, `empty_disjUnion`, `mem_disjUnion`, `not_disjoint_iff`, `pairwiseDisjoint_coe`, `pairwiseDisjoint_singleton_iff_injOn`, `singleton_disjUnion`, `disjoint_toFinset_iff_disjoint`, `disjoint_toFinset`	33
Total	35

Disjoint

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`forall_ne_finset` 📖	—	`Disjoint` `Finset` `Finset.partialOrder` `Finset.instOrderBot` `Finset.instMembership`	—	—	`Finset.disjoint_iff_ne`
`notMem_of_mem_left_finset` 📖	—	`Disjoint` `Finset` `Finset.partialOrder` `Finset.instOrderBot` `Finset.instMembership`	—	—	`Finset.disjoint_left`
`notMem_of_mem_right_finset` 📖	—	`Disjoint` `Finset` `Finset.partialOrder` `Finset.instOrderBot` `Finset.instMembership`	—	—	`Finset.disjoint_right`

Finset

Definitions

Name	Category	Theorems
`decidableDisjoint` 📖	CompOp	3 math math: `Set.Sized.uvCompression`, `UV.card_compress`, `UV.toColex_compress_lt_toColex`
`disjUnion` 📖	CompOp	38 math math: `disjUnion_singleton`, `Ioi_disjUnion_Iio`, `pairwiseDisjoint_disjUnion`, `singleton_disjUnion`, `disjUnion_inj_right`, `box_succ_disjUnion`, `disjUnion_product`, `disjUnion_empty`, `disjUnion_val`, `empty_disjUnion`, `disjUnion_inj_left`, `filter_disjUnion`, `Int.divisorsAntidiag_natCast`, `sum_disjUnion`, `disjiUnion_disjUnion`, `SimpleGraph.neighborFinset_boxProd`, `fold_disjUnion`, `map_inl_disjUnion_map_inr`, `product_disjUnion`, `UniqueFactorizationMonoid.primeFactors_mul_eq_disjUnion`, `prod_disjUnion`, `sym2_cons`, `mem_disjUnion`, `map_disjSum`, `dens_disjUnion`, `Int.divisorsAntidiag_ofNat`, `Finsupp.piecewise_support`, `card_disjUnion`, `disjUnion_eq_union`, `map_disjUnion'`, `Equiv.Perm.ofSign_disjUnion`, `disjoint_disjUnion_left`, `map_disjUnion`, `disjiUnion_cons`, `disjoint_disjUnion_right`, `Int.divisorsAntidiag_neg_natCast`, `disjUnion_comm`, `coe_disjUnion`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_disjUnion` 📖	mathematical	`Disjoint` `Finset` `partialOrder` `instOrderBot`	`SetLike.coe` `instSetLike` `disjUnion` `Set` `Set.instUnion`	—	`Set.ext`
`disjUnion_comm` 📖	mathematical	`Disjoint` `Finset` `partialOrder` `instOrderBot`	`disjUnion` `Disjoint.symm`	—	`eq_of_veq` `Disjoint.symm` `Multiset.add_comm`
`disjUnion_empty` 📖	mathematical	`Disjoint` `Finset` `partialOrder` `instOrderBot` `instEmptyCollection` `disjoint_bot_right`	`disjUnion`	—	`eq_of_veq` `Multiset.add_zero`
`disjUnion_inj_left` 📖	mathematical	`Disjoint` `Finset` `partialOrder` `instOrderBot`	`disjUnion`	—	—
`disjUnion_inj_right` 📖	mathematical	`Disjoint` `Finset` `partialOrder` `instOrderBot`	`disjUnion`	—	—
`disjUnion_singleton` 📖	mathematical	`Disjoint` `Finset` `partialOrder` `instOrderBot` `instSingleton`	`disjUnion` `cons` `instMembership` `disjoint_singleton_right`	—	`disjoint_singleton_right` `Disjoint.symm` `disjUnion_comm` `disjoint_singleton_left` `singleton_disjUnion`
`disjUnion_val` 📖	mathematical	`Disjoint` `Finset` `partialOrder` `instOrderBot`	`val` `disjUnion` `Multiset` `Multiset.instAdd`	—	—
`disjoint_coe` 📖	mathematical	—	`Disjoint` `Set` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `Set.instBooleanAlgebra` `HeytingAlgebra.toOrderBot` `BiheytingAlgebra.toHeytingAlgebra` `SetLike.coe` `Finset` `instSetLike` `partialOrder` `instOrderBot`	—	—
`disjoint_empty_left` 📖	mathematical	—	`Disjoint` `Finset` `partialOrder` `instOrderBot` `instEmptyCollection`	—	`disjoint_bot_left`
`disjoint_empty_right` 📖	mathematical	—	`Disjoint` `Finset` `partialOrder` `instOrderBot` `instEmptyCollection`	—	`disjoint_bot_right`
`disjoint_iff_ne` 📖	mathematical	—	`Disjoint` `Finset` `partialOrder` `instOrderBot`	—	—
`disjoint_insert_left` 📖	mathematical	—	`Disjoint` `Finset` `partialOrder` `instOrderBot` `instInsert` `instMembership`	—	—
`disjoint_insert_right` 📖	mathematical	—	`Disjoint` `Finset` `partialOrder` `instOrderBot` `instInsert` `instMembership`	—	`disjoint_comm` `disjoint_insert_left`
`disjoint_left` 📖	mathematical	—	`Disjoint` `Finset` `partialOrder` `instOrderBot` `instMembership`	—	`notMem_empty` `singleton_subset_iff`
`disjoint_of_subset_left` 📖	—	`Finset` `instHasSubset` `Disjoint` `partialOrder` `instOrderBot`	—	—	`disjoint_left`
`disjoint_of_subset_right` 📖	—	`Finset` `instHasSubset` `Disjoint` `partialOrder` `instOrderBot`	—	—	`disjoint_right`
`disjoint_right` 📖	mathematical	—	`Disjoint` `Finset` `partialOrder` `instOrderBot` `instMembership`	—	`disjoint_comm` `disjoint_left`
`disjoint_self_iff_empty` 📖	mathematical	—	`Disjoint` `Finset` `partialOrder` `instOrderBot` `instEmptyCollection`	—	`disjoint_self`
`disjoint_singleton` 📖	mathematical	—	`Disjoint` `Finset` `partialOrder` `instOrderBot` `instSingleton`	—	`disjoint_singleton_left` `mem_singleton`
`disjoint_singleton_left` 📖	mathematical	—	`Disjoint` `Finset` `partialOrder` `instOrderBot` `instSingleton` `instMembership`	—	—
`disjoint_singleton_right` 📖	mathematical	—	`Disjoint` `Finset` `partialOrder` `instOrderBot` `instSingleton` `instMembership`	—	`disjoint_comm` `disjoint_singleton_left`
`disjoint_val` 📖	mathematical	—	`Disjoint` `Multiset` `Multiset.instPartialOrder` `Multiset.instOrderBot` `val` `Finset` `partialOrder` `instOrderBot`	—	`Multiset.disjoint_left` `disjoint_left`
`empty_disjUnion` 📖	mathematical	`Disjoint` `Finset` `partialOrder` `instOrderBot` `instEmptyCollection` `disjoint_bot_left`	`disjUnion`	—	`eq_of_veq` `Multiset.zero_add`
`mem_disjUnion` 📖	mathematical	`Disjoint` `Finset` `partialOrder` `instOrderBot`	`instMembership` `disjUnion`	—	—
`not_disjoint_iff` 📖	mathematical	—	`Disjoint` `Finset` `partialOrder` `instOrderBot` `instMembership`	—	`Iff.not` `disjoint_left`
`pairwiseDisjoint_coe` 📖	mathematical	—	`Set.PairwiseDisjoint` `Set` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `Set.instBooleanAlgebra` `HeytingAlgebra.toOrderBot` `BiheytingAlgebra.toHeytingAlgebra` `SetLike.coe` `Finset` `instSetLike` `partialOrder` `instOrderBot`	—	`disjoint_coe`
`pairwiseDisjoint_singleton_iff_injOn` 📖	mathematical	—	`Set.PairwiseDisjoint` `Finset` `partialOrder` `instOrderBot` `instSingleton` `Set.InjOn`	—	—
`singleton_disjUnion` 📖	mathematical	`Disjoint` `Finset` `partialOrder` `instOrderBot` `instSingleton`	`disjUnion` `cons` `instMembership` `disjoint_singleton_left`	—	`eq_of_veq` `disjoint_singleton_left` `Multiset.singleton_add`

List

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`disjoint_toFinset_iff_disjoint` 📖	mathematical	—	`Disjoint` `Finset` `Finset.partialOrder` `Finset.instOrderBot` `toFinset`	—	`Multiset.disjoint_toFinset` `Multiset.coe_disjoint`

Multiset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`disjoint_toFinset` 📖	mathematical	—	`Disjoint` `Finset` `Finset.partialOrder` `Finset.instOrderBot` `toFinset` `Multiset` `instPartialOrder` `instOrderBot`	—	—

---

← Back to Index