Option

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

Statistics

Metric	Count
Definitions truncRecEmptyOption, fintypeOfOption, fintypeOfOptionEquiv, instFintypeOption	4
Theorems induction_empty_option, card_option, induction_empty_option, instFiniteOption, univ_option	5
Total	9

Finite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
induction_empty_option 📖	—	—	—	—	nonempty_fintype Fintype.induction_empty_option

Fintype

Definitions

Name	Category	Theorems
truncRecEmptyOption 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
card_option 📖	mathematical	—	card instFintypeOption	—	Finset.card_cons Finset.card_map
induction_empty_option 📖	—	instPEmpty instFintypeOption	—	—	Lean.Meta.FastSubsingleton.elim instFastSubsingleton

(root)

Definitions

Name	Category	Theorems
fintypeOfOption 📖	CompOp	—
fintypeOfOptionEquiv 📖	CompOp	—
instFintypeOption 📖	CompOp	11 math math: Fintype.prod_option, ContinuousLinearMap.hasFiniteFPowerSeriesOnBall_uncurry_of_multilinear, Fintype.sum_option, Finset.univ_perm_option, CompleteOrthogonalIdempotents.option, Fintype.card_option, Equiv.Perm.decomposeOption_symm_sign, univ_option, MeasureTheory.Measure.pi_map_piOptionEquivProd, Equiv.optionCongr_sign, Turing.PartrecToTM2.supports_biUnion

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instFiniteOption 📖	mathematical	—	Finite	—	Finite.of_fintype
univ_option 📖	mathematical	—	Finset.univ instFintypeOption DFunLike.coe OrderEmbedding Finset Preorder.toLE PartialOrder.toPreorder Finset.partialOrder instFunLikeOrderEmbedding Finset.insertNone	—	—

---

← Back to Index