Option

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

Statistics

Metric	Count
Definitions `eraseNone`, `insertNone`, `toFinset`	3
Theorems `card_eraseNone_eq_card_erase`, `card_eraseNone_le`, `card_eraseNone_of_mem`, `card_eraseNone_of_not_mem`, `card_insertNone`, `coe_eraseNone`, `eraseNone_empty`, `eraseNone_eq_biUnion`, `eraseNone_image_some`, `eraseNone_insertNone`, `eraseNone_inter`, `eraseNone_map_some`, `eraseNone_none`, `eraseNone_union`, `forall_mem_eraseNone`, `forall_mem_insertNone`, `image_some_eraseNone`, `insertNone_eraseNone`, `insertNone_nonempty`, `map_some_eraseNone`, `mem_eraseNone`, `mem_insertNone`, `none_mem_insertNone`, `some_mem_insertNone`, `card_toFinset`, `mem_toFinset`, `toFinset_none`, `toFinset_some`	28
Total	31

Finset

Definitions

Name	Category	Theorems
`eraseNone` 📖	CompOp	19 math math: `insertNone_eraseNone`, `card_eraseNone_le`, `eraseNone_union`, `eraseNone_none`, `card_eraseNone_of_not_mem`, `card_eraseNone_of_mem`, `image_some_eraseNone`, `eraseNone_map_some`, `sum_eraseNone`, `coe_eraseNone`, `eraseNone_eq_biUnion`, `prod_eraseNone`, `eraseNone_image_some`, `eraseNone_inter`, `card_eraseNone_eq_card_erase`, `mem_eraseNone`, `eraseNone_empty`, `eraseNone_insertNone`, `map_some_eraseNone`
`insertNone` 📖	CompOp	16 math math: `add_sum_eq_sum_insertNone`, `card_insertNone`, `insertNone_eraseNone`, `WithBot.Ico_bot_coe`, `none_mem_insertNone`, `mul_prod_eq_prod_insertNone`, `sum_insertNone`, `some_mem_insertNone`, `prod_insertNone`, `insertNone_nonempty`, `univ_option`, `WithTop.Ioc_coe_top`, `WithTop.Icc_coe_top`, `eraseNone_insertNone`, `WithBot.Icc_bot_coe`, `mem_insertNone`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_eraseNone_eq_card_erase` 📖	mathematical	—	`card` `DFunLike.coe` `OrderHom` `Finset` `PartialOrder.toPreorder` `partialOrder` `OrderHom.instFunLike` `eraseNone` `erase`	—	`card_map` `map_some_eraseNone`
`card_eraseNone_le` 📖	mathematical	—	`card` `DFunLike.coe` `OrderHom` `Finset` `PartialOrder.toPreorder` `partialOrder` `OrderHom.instFunLike` `eraseNone`	—	`card_eraseNone_eq_card_erase` `card_erase_le`
`card_eraseNone_of_mem` 📖	mathematical	`Finset` `instMembership`	`card` `DFunLike.coe` `OrderHom` `PartialOrder.toPreorder` `partialOrder` `OrderHom.instFunLike` `eraseNone`	—	`card_eraseNone_eq_card_erase` `card_erase_of_mem`
`card_eraseNone_of_not_mem` 📖	mathematical	`Finset` `instMembership`	`card` `DFunLike.coe` `OrderHom` `PartialOrder.toPreorder` `partialOrder` `OrderHom.instFunLike` `eraseNone`	—	`card_eraseNone_eq_card_erase` `erase_eq_of_notMem`
`card_insertNone` 📖	mathematical	—	`card` `DFunLike.coe` `OrderEmbedding` `Finset` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `instFunLikeOrderEmbedding` `insertNone`	—	`card_cons` `card_map`
`coe_eraseNone` 📖	mathematical	—	`SetLike.coe` `Finset` `instSetLike` `DFunLike.coe` `OrderHom` `PartialOrder.toPreorder` `partialOrder` `OrderHom.instFunLike` `eraseNone` `Set.preimage`	—	`Set.ext` `mem_eraseNone`
`eraseNone_empty` 📖	mathematical	—	`DFunLike.coe` `OrderHom` `Finset` `PartialOrder.toPreorder` `partialOrder` `OrderHom.instFunLike` `eraseNone` `instEmptyCollection`	—	`ext`
`eraseNone_eq_biUnion` 📖	mathematical	—	`DFunLike.coe` `OrderHom` `Finset` `PartialOrder.toPreorder` `partialOrder` `OrderHom.instFunLike` `eraseNone` `biUnion` `Option.toFinset`	—	`ext`
`eraseNone_image_some` 📖	mathematical	—	`DFunLike.coe` `OrderHom` `Finset` `PartialOrder.toPreorder` `partialOrder` `OrderHom.instFunLike` `eraseNone` `image`	—	`map_eq_image` `eraseNone_map_some`
`eraseNone_insertNone` 📖	mathematical	—	`DFunLike.coe` `OrderHom` `Finset` `PartialOrder.toPreorder` `partialOrder` `OrderHom.instFunLike` `eraseNone` `OrderEmbedding` `Preorder.toLE` `instFunLikeOrderEmbedding` `insertNone`	—	`ext`
`eraseNone_inter` 📖	mathematical	—	`DFunLike.coe` `OrderHom` `Finset` `PartialOrder.toPreorder` `partialOrder` `OrderHom.instFunLike` `eraseNone` `instInter`	—	`ext`
`eraseNone_map_some` 📖	mathematical	—	`DFunLike.coe` `OrderHom` `Finset` `PartialOrder.toPreorder` `partialOrder` `OrderHom.instFunLike` `eraseNone` `map` `Function.Embedding.some`	—	`ext`
`eraseNone_none` 📖	mathematical	—	`DFunLike.coe` `OrderHom` `Finset` `PartialOrder.toPreorder` `partialOrder` `OrderHom.instFunLike` `eraseNone` `instSingleton` `instEmptyCollection`	—	`ext`
`eraseNone_union` 📖	mathematical	—	`DFunLike.coe` `OrderHom` `Finset` `PartialOrder.toPreorder` `partialOrder` `OrderHom.instFunLike` `eraseNone` `instUnion`	—	`ext`
`forall_mem_eraseNone` 📖	—	—	—	—	—
`forall_mem_insertNone` 📖	—	—	—	—	`instIsEmptyFalse`
`image_some_eraseNone` 📖	mathematical	—	`image` `DFunLike.coe` `OrderHom` `Finset` `PartialOrder.toPreorder` `partialOrder` `OrderHom.instFunLike` `eraseNone` `erase`	—	`ext`
`insertNone_eraseNone` 📖	mathematical	—	`DFunLike.coe` `OrderEmbedding` `Finset` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `instFunLikeOrderEmbedding` `insertNone` `OrderHom` `OrderHom.instFunLike` `eraseNone` `instInsert`	—	`ext` `instIsEmptyFalse`
`insertNone_nonempty` 📖	mathematical	—	`Nonempty` `DFunLike.coe` `OrderEmbedding` `Finset` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `instFunLikeOrderEmbedding` `insertNone`	—	`none_mem_insertNone`
`map_some_eraseNone` 📖	mathematical	—	`map` `Function.Embedding.some` `DFunLike.coe` `OrderHom` `Finset` `PartialOrder.toPreorder` `partialOrder` `OrderHom.instFunLike` `eraseNone` `erase`	—	`map_eq_image` `Function.Embedding.some_apply` `image_some_eraseNone`
`mem_eraseNone` 📖	mathematical	—	`Finset` `instMembership` `DFunLike.coe` `OrderHom` `PartialOrder.toPreorder` `partialOrder` `OrderHom.instFunLike` `eraseNone`	—	—
`mem_insertNone` 📖	mathematical	—	`Finset` `instMembership` `DFunLike.coe` `OrderEmbedding` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `instFunLikeOrderEmbedding` `insertNone`	—	`Multiset.mem_cons_self` `Multiset.mem_cons` `Multiset.map_congr`
`none_mem_insertNone` 📖	mathematical	—	`Finset` `instMembership` `DFunLike.coe` `OrderEmbedding` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `instFunLikeOrderEmbedding` `insertNone`	—	`instIsEmptyFalse`
`some_mem_insertNone` 📖	mathematical	—	`Finset` `instMembership` `DFunLike.coe` `OrderEmbedding` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `instFunLikeOrderEmbedding` `insertNone`	—	—

Option

Definitions

Name	Category	Theorems
`toFinset` 📖	CompOp	10 math math: `toFinset_none`, `toFinset_some`, `Finmap.sigma_keys_lookup`, `Finset.eraseNone_eq_biUnion`, `card_toFinset`, `Finset.set_biUnion_option_toFinset`, `mem_toFinset`, `Finset.iSup_option_toFinset`, `Finset.set_biInter_option_toFinset`, `Finset.iInf_option_toFinset`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_toFinset` 📖	mathematical	—	`Finset.card` `toFinset` `Pi.instOne` `Nat.instOne`	—	—
`mem_toFinset` 📖	mathematical	—	`Finset` `Finset.instMembership` `toFinset`	—	—
`toFinset_none` 📖	mathematical	—	`toFinset` `Finset` `Finset.instEmptyCollection`	—	—
`toFinset_some` 📖	mathematical	—	`toFinset` `Finset` `Finset.instSingleton`	—	—

---

← Back to Index