Defs

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

Statistics

Metric	Count
Definitions elim', iget, traverse	3
Theorems elim'_eq_elim, elim'_none, elim'_none_some, elim'_some, iget_some	5
Total	8

Option

Definitions

Name	Category	Theorems
elim' 📖	CompOp	19 math math: partialFunToPointed_map, BoxIntegral.BoxAdditiveMap.map_split_add, elim'_eq_elim, LocallyFinite.option_elim', Function.Embedding.optionElim_apply, elim'_none_some, partialFunEquivPointed_functor_map_toFun, elim'_none, Finsupp.optionElim_eq_elim', Finset.sum_eraseNone, IsLocalExtrOn.linear_dependent_of_hasStrictFDerivAt, Dioph.ex1_dioph, Dioph.diophFn_comp1, Finset.prod_eraseNone, Dioph.diophPFun_comp1, BoxIntegral.Prepartition.sum_split_boxes, elim'_some, elim'_update, BoxIntegral.Prepartition.sum_ofWithBot
iget 📖	CompOp	5 math math: getD_default_eq_iget, Primrec.option_iget, iget_some, iget_of_mem, iget_mem
traverse 📖	CompOp	4 math math: naturality, id_traverse, traverse_eq_map_id, comp_traverse

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
elim'_eq_elim 📖	mathematical	—	elim'	—	—
elim'_none 📖	mathematical	—	elim'	—	—
elim'_none_some 📖	mathematical	—	elim'	—	—
elim'_some 📖	mathematical	—	elim'	—	—
iget_some 📖	mathematical	—	iget	—	—

---

← Back to Index