Theorems · Definition · combinatorics
Finset.eraseNone
{α : Type u_1} → Finset (Option α) →o Finset αGiven s : Finset (Option α), eraseNone s : Finset α is the set of x : α such that
some x ∈ s.
- Defined in
- Mathlib.Data.Finset.Option
- Cited by
- 21 results in Mathlib
- Foundations
- Depth 61 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Finsetstatement · cited by 13,712
- OrderHomstatement · cited by 934
- Equiv.toEmbeddingproof · cited by 254
- OrderHom.compproof · cited by 61
- Finset.subtypeproof · cited by 41
- OrderEmbedding.toOrderHomproof · cited by 16
- Finset.mapEmbeddingproof · cited by 8
- Equiv.optionIsSomeEquivproof · cited by 3
Cited by23
Results whose statement or proof uses this declaration.
- BoxIntegral.Prepartition.ofWithBotproof · cited by 7
- Finset.map_some_eraseNonestatement and proof · cited by 3
- Finset.card_eraseNone_eq_card_erasestatement · cited by 3
- Finset.mem_eraseNonestatement · cited by 2
- BoxIntegral.Prepartition.restrict_boxes_of_leproof · cited by 1
- Finset.eraseNone_eq_biUnionstatement · cited by 1
- Finset.eraseNone_map_somestatement · cited by 1
- Finset.image_some_eraseNonestatement · cited by 1
- Finset.sum_eraseNonestatement and proof · cited by 1
- Finset.prod_eraseNonestatement and proof · cited by 0
- fintypeOfOptionproof · cited by 0
- Finset.eraseNone_emptystatement · cited by 0