Basic

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

Statistics

Metric	Count
Definitions `casesOn'`	1
Theorems `leftUnique`, `bind_congr'`, `bind_eq_bind'`, `bind_pmap`, `casesOn'_coe`, `casesOn'_eq_elim`, `casesOn'_none`, `casesOn'_none_coe`, `casesOn'_some`, `choice_eq_none`, `coe_def`, `coe_get`, `elim'_update`, `elim_apply`, `elim_comp`, `elim_comp₂`, `elim_none_some`, `eq_of_mem_of_mem`, `exists_mem_map`, `failure_eq_none`, `forall_mem_map`, `getD_comp_some`, `getD_default_eq_iget`, `guard_eq_some'`, `iget_mem`, `iget_of_mem`, `joinM_eq_join`, `join_pmap_eq_pmap_join`, `map_coe`, `map_coe'`, `map_comm`, `map_comp_some`, `map_eq_id`, `map_inj`, `map_injective'`, `mem_map`, `mem_map_of_injective`, `mem_pmem`, `orElse_eq_none`, `orElse_eq_some`, `pbind_eq_none`, `pmap_bind`, `pmap_bind_id_eq_pmap_join`, `seq_some`, `some_injective`	45
Total	46

Option

Definitions

Name	Category	Theorems
`casesOn'` 📖	CompOp	9 math math: `LinearIndependent.option`, `casesOn'_some`, `casesOn'_coe`, `casesOn'_none_coe`, `casesOn'_none`, `partialFunEquivPointed_counitIso_hom_app_toFun`, `linearIndependent_option'`, `Equiv.optionSubtypeNe_apply`, `casesOn'_eq_elim`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bind_congr'` 📖	—	—	—	—	—
`bind_eq_bind'` 📖	—	—	—	—	—
`bind_pmap` 📖	—	—	—	—	—
`casesOn'_coe` 📖	mathematical	—	`casesOn'`	—	—
`casesOn'_eq_elim` 📖	mathematical	—	`casesOn'`	—	—
`casesOn'_none` 📖	mathematical	—	`casesOn'`	—	—
`casesOn'_none_coe` 📖	mathematical	—	`casesOn'`	—	—
`casesOn'_some` 📖	mathematical	—	`casesOn'`	—	—
`choice_eq_none` 📖	—	—	—	—	`not_nonempty_iff_imp_false`
`coe_def` 📖	—	—	—	—	—
`coe_get` 📖	—	—	—	—	—
`elim'_update` 📖	mathematical	—	`elim'` `Function.update`	—	`Function.rec_update`
`elim_apply` 📖	—	—	—	—	`elim_comp`
`elim_comp` 📖	—	—	—	—	—
`elim_comp₂` 📖	—	—	—	—	—
`elim_none_some` 📖	—	—	—	—	—
`eq_of_mem_of_mem` 📖	—	—	—	—	—
`exists_mem_map` 📖	—	—	—	—	—
`failure_eq_none` 📖	—	—	—	—	—
`forall_mem_map` 📖	—	—	—	—	—
`getD_comp_some` 📖	—	—	—	—	—
`getD_default_eq_iget` 📖	mathematical	—	`iget`	—	—
`guard_eq_some'` 📖	—	—	—	—	—
`iget_mem` 📖	mathematical	—	`iget`	—	—
`iget_of_mem` 📖	mathematical	—	`iget`	—	—
`joinM_eq_join` 📖	mathematical	—	`joinM`	—	—
`join_pmap_eq_pmap_join` 📖	—	—	—	—	—
`map_coe` 📖	—	—	—	—	—
`map_coe'` 📖	—	—	—	—	—
`map_comm` 📖	—	—	—	—	—
`map_comp_some` 📖	—	—	—	—	—
`map_eq_id` 📖	—	—	—	—	`map_injective'`
`map_inj` 📖	—	—	—	—	`map_injective'`
`map_injective'` 📖	—	—	—	—	`some_injective`
`mem_map` 📖	—	—	—	—	—
`mem_map_of_injective` 📖	—	—	—	—	—
`mem_pmem` 📖	—	—	—	—	—
`orElse_eq_none` 📖	—	—	—	—	—
`orElse_eq_some` 📖	—	—	—	—	—
`pbind_eq_none` 📖	—	—	—	—	—
`pmap_bind` 📖	—	—	—	—	—
`pmap_bind_id_eq_pmap_join` 📖	—	—	—	—	—
`seq_some` 📖	—	—	—	—	—
`some_injective` 📖	—	—	—	—	—

Option.Mem

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`leftUnique` 📖	mathematical	—	`Relator.LeftUnique`	—	—

---

← Back to Index