Lemmas

📁 Source: Mathlib/Data/Finset/Lattice/Lemmas.lean

Statistics

Metric	Count
Definitions	0
Theorems `inl`, `inr`, `disjoint_iff_inter_eq_empty`, `empty_inter`, `empty_union`, `induction_on_union`, `insert_eq`, `insert_inter`, `insert_inter_of_mem`, `insert_inter_of_notMem`, `insert_union`, `insert_union_comm`, `insert_union_distrib`, `inter_empty`, `inter_insert`, `inter_insert_of_mem`, `inter_insert_of_notMem`, `inter_singleton`, `inter_singleton_of_mem`, `inter_singleton_of_notMem`, `singleton_inter`, `singleton_inter_of_mem`, `singleton_inter_of_notMem`, `singleton_union`, `union_empty`, `union_eq_empty`, `union_insert`, `union_nonempty`, `union_singleton`, `toFinset_append`	30
Total	30

Finset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`disjoint_iff_inter_eq_empty` 📖	mathematical	—	`Disjoint` `Finset` `partialOrder` `instOrderBot` `instInter` `instEmptyCollection`	—	`disjoint_iff`
`empty_inter` 📖	mathematical	—	`Finset` `instInter` `instEmptyCollection`	—	`ext` `mem_inter`
`empty_union` 📖	mathematical	—	`Finset` `instUnion` `instEmptyCollection`	—	`ext` `mem_union`
`induction_on_union` 📖	—	`Finset` `instEmptyCollection` `instSingleton` `instUnion`	—	—	`induction_on` `insert_eq`
`insert_eq` 📖	mathematical	—	`Finset` `instInsert` `instUnion` `instSingleton`	—	—
`insert_inter` 📖	mathematical	—	`Finset` `instInter` `instInsert` `instMembership` `decidableMem`	—	`inter_insert_of_mem` `inter_insert_of_notMem`
`insert_inter_of_mem` 📖	mathematical	`Finset` `instMembership`	`instInter` `instInsert`	—	`ext`
`insert_inter_of_notMem` 📖	mathematical	`Finset` `instMembership`	`instInter` `instInsert`	—	`ext`
`insert_union` 📖	mathematical	—	`Finset` `instUnion` `instInsert`	—	`union_assoc`
`insert_union_comm` 📖	mathematical	—	`Finset` `instUnion` `instInsert`	—	`insert_union` `union_insert`
`insert_union_distrib` 📖	mathematical	—	`Finset` `instInsert` `instUnion`	—	`union_insert` `insert_union` `insert_idem`
`inter_empty` 📖	mathematical	—	`Finset` `instInter` `instEmptyCollection`	—	`ext` `mem_inter`
`inter_insert` 📖	mathematical	—	`Finset` `instInter` `instInsert` `instMembership` `decidableMem`	—	`insert_inter_of_mem` `insert_inter_of_notMem`
`inter_insert_of_mem` 📖	mathematical	`Finset` `instMembership`	`instInter` `instInsert`	—	`inter_comm` `insert_inter_of_mem`
`inter_insert_of_notMem` 📖	mathematical	`Finset` `instMembership`	`instInter` `instInsert`	—	`inter_comm` `insert_inter_of_notMem`
`inter_singleton` 📖	mathematical	—	`Finset` `instInter` `instSingleton` `instMembership` `decidableMem` `instEmptyCollection`	—	`inter_singleton_of_mem` `inter_singleton_of_notMem`
`inter_singleton_of_mem` 📖	mathematical	`Finset` `instMembership`	`instInter` `instSingleton`	—	`inter_comm` `singleton_inter_of_mem`
`inter_singleton_of_notMem` 📖	mathematical	`Finset` `instMembership`	`instInter` `instSingleton` `instEmptyCollection`	—	`inter_comm` `singleton_inter_of_notMem`
`singleton_inter` 📖	mathematical	—	`Finset` `instInter` `instSingleton` `instMembership` `decidableMem` `instEmptyCollection`	—	`singleton_inter_of_mem` `singleton_inter_of_notMem`
`singleton_inter_of_mem` 📖	mathematical	`Finset` `instMembership`	`instInter` `instSingleton`	—	`insert_inter_of_mem` `empty_inter`
`singleton_inter_of_notMem` 📖	mathematical	`Finset` `instMembership`	`instInter` `instSingleton` `instEmptyCollection`	—	`eq_empty_of_forall_notMem`
`singleton_union` 📖	mathematical	—	`Finset` `instUnion` `instSingleton` `instInsert`	—	—
`union_empty` 📖	mathematical	—	`Finset` `instUnion` `instEmptyCollection`	—	`ext` `mem_union`
`union_eq_empty` 📖	mathematical	—	`Finset` `instUnion` `instEmptyCollection`	—	`sup_eq_bot_iff`
`union_insert` 📖	mathematical	—	`Finset` `instUnion` `instInsert`	—	`union_left_comm`
`union_nonempty` 📖	mathematical	—	`Nonempty` `Finset` `instUnion`	—	`Set.union_nonempty`
`union_singleton` 📖	mathematical	—	`Finset` `instUnion` `instSingleton` `instInsert`	—	`union_comm` `singleton_union`

Finset.Nonempty

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`inl` 📖	mathematical	`Finset.Nonempty`	`Finset` `Finset.instUnion`	—	`mono` `Finset.subset_union_left`
`inr` 📖	mathematical	`Finset.Nonempty`	`Finset` `Finset.instUnion`	—	`mono` `Finset.subset_union_right`

List

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toFinset_append` 📖	mathematical	—	`toFinset` `Finset` `Finset.instUnion`	—	`Finset.empty_union` `toFinset_cons` `Finset.insert_union`

---

← Back to Index