Option

📁 Source: Mathlib/Logic/Equiv/Option.lean

Statistics

Metric	Count
Definitions `optionCongr`, `optionEquivSumPUnit`, `optionIsSomeEquiv`, `optionSubtype`, `optionSubtypeNe`, `removeNone`, `removeNone_aux`	7
Theorems `coe_optionSubtype_apply_apply`, `optionCongr_apply`, `optionCongr_eq_equivFunctor_mapEquiv`, `optionCongr_injective`, `optionCongr_refl`, `optionCongr_symm`, `optionCongr_trans`, `optionEquivSumPUnit_coe`, `optionEquivSumPUnit_none`, `optionEquivSumPUnit_some`, `optionEquivSumPUnit_symm_inl`, `optionEquivSumPUnit_symm_inr`, `optionIsSomeEquiv_apply`, `optionIsSomeEquiv_symm_apply_coe`, `optionSubtypeNe_apply`, `optionSubtypeNe_none`, `optionSubtypeNe_some`, `optionSubtypeNe_symm_apply`, `optionSubtypeNe_symm_of_ne`, `optionSubtypeNe_symm_self`, `optionSubtype_apply_apply`, `optionSubtype_apply_symm_apply`, `optionSubtype_symm_apply_apply_coe`, `optionSubtype_symm_apply_apply_none`, `optionSubtype_symm_apply_apply_some`, `optionSubtype_symm_apply_symm_apply`, `option_symm_apply_none_iff`, `removeNone_aux_inv`, `removeNone_aux_none`, `removeNone_aux_some`, `removeNone_none`, `removeNone_optionCongr`, `removeNone_some`, `removeNone_symm`, `some_removeNone_iff`	35
Total	42

Equiv

Definitions

Name	Category	Theorems
`optionCongr` 📖	CompOp	13 math math: `map_equiv_removeNone`, `removeNone_optionCongr`, `optionCongr_one`, `optionCongr_injective`, `optionCongr_refl`, `optionCongr_swap`, `optionCongr_trans`, `optionCongr_apply`, `MvPolynomial.finSuccEquiv_rename_finSuccEquiv`, `Perm.decomposeOption_symm_apply`, `optionCongr_sign`, `optionCongr_eq_equivFunctor_mapEquiv`, `optionCongr_symm`
`optionEquivSumPUnit` 📖	CompOp	5 math math: `optionEquivSumPUnit_symm_inr`, `optionEquivSumPUnit_none`, `optionEquivSumPUnit_symm_inl`, `optionEquivSumPUnit_coe`, `optionEquivSumPUnit_some`
`optionIsSomeEquiv` 📖	CompOp	2 math math: `optionIsSomeEquiv_symm_apply_coe`, `optionIsSomeEquiv_apply`
`optionSubtype` 📖	CompOp	7 math math: `optionSubtype_symm_apply_apply_coe`, `optionSubtype_apply_symm_apply`, `optionSubtype_symm_apply_apply_none`, `optionSubtype_apply_apply`, `coe_optionSubtype_apply_apply`, `optionSubtype_symm_apply_apply_some`, `optionSubtype_symm_apply_symm_apply`
`optionSubtypeNe` 📖	CompOp	7 math math: `optionSubtypeNe_symm_of_ne`, `optionSubtypeNe_symm_apply`, `optionSubtypeNe_some`, `optionSubtypeNe_none`, `MvPolynomial.degreeOf_eq_natDegree`, `optionSubtypeNe_apply`, `optionSubtypeNe_symm_self`
`removeNone` 📖	CompOp	8 math math: `map_equiv_removeNone`, `removeNone_optionCongr`, `derangements.Equiv.RemoveNone.mem_fiber`, `removeNone_none`, `removeNone_symm`, `Perm.decomposeOption_apply`, `removeNone_some`, `some_removeNone_iff`
`removeNone_aux` 📖	CompOp	3 math math: `removeNone_aux_none`, `removeNone_aux_inv`, `removeNone_aux_some`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_optionSubtype_apply_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `instEquivLike` `optionSubtype`	—	—
`optionCongr_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `instEquivLike` `optionCongr`	—	—
`optionCongr_eq_equivFunctor_mapEquiv` 📖	mathematical	—	`optionCongr` `EquivFunctor.mapEquiv` `EquivFunctor.ofLawfulFunctor`	—	—
`optionCongr_injective` 📖	mathematical	—	`Equiv` `optionCongr`	—	`removeNone_optionCongr`
`optionCongr_refl` 📖	mathematical	—	`optionCongr` `refl`	—	`ext`
`optionCongr_symm` 📖	mathematical	—	`optionCongr` `symm`	—	—
`optionCongr_trans` 📖	mathematical	—	`optionCongr` `trans`	—	`ext`
`optionEquivSumPUnit_coe` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `instEquivLike` `optionEquivSumPUnit`	—	—
`optionEquivSumPUnit_none` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `instEquivLike` `optionEquivSumPUnit`	—	—
`optionEquivSumPUnit_some` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `instEquivLike` `optionEquivSumPUnit`	—	—
`optionEquivSumPUnit_symm_inl` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `instEquivLike` `symm` `optionEquivSumPUnit`	—	—
`optionEquivSumPUnit_symm_inr` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `instEquivLike` `symm` `optionEquivSumPUnit`	—	—
`optionIsSomeEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `instEquivLike` `optionIsSomeEquiv`	—	—
`optionIsSomeEquiv_symm_apply_coe` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `instEquivLike` `symm` `optionIsSomeEquiv`	—	—
`optionSubtypeNe_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `instEquivLike` `optionSubtypeNe` `Option.casesOn'`	—	—
`optionSubtypeNe_none` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `instEquivLike` `optionSubtypeNe`	—	—
`optionSubtypeNe_some` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `instEquivLike` `optionSubtypeNe`	—	—
`optionSubtypeNe_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `instEquivLike` `symm` `optionSubtypeNe`	—	—
`optionSubtypeNe_symm_of_ne` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `instEquivLike` `symm` `optionSubtypeNe`	—	—
`optionSubtypeNe_symm_self` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `instEquivLike` `symm` `optionSubtypeNe`	—	—
`optionSubtype_apply_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `instEquivLike` `optionSubtype`	—	—
`optionSubtype_apply_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `instEquivLike` `symm` `optionSubtype`	—	—
`optionSubtype_symm_apply_apply_coe` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `instEquivLike` `symm` `optionSubtype`	—	—
`optionSubtype_symm_apply_apply_none` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `instEquivLike` `symm` `optionSubtype`	—	—
`optionSubtype_symm_apply_apply_some` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `instEquivLike` `symm` `optionSubtype`	—	—
`optionSubtype_symm_apply_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `instEquivLike` `symm` `optionSubtype`	—	`Subtype.coe_eta`
`option_symm_apply_none_iff` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `instEquivLike` `symm`	—	`apply_symm_apply` `symm_apply_apply`
`removeNone_aux_inv` 📖	mathematical	—	`removeNone_aux` `symm`	—	`Option.some_injective` `removeNone_aux_none` `eq_symm_apply` `symm_apply_apply` `removeNone_aux_some`
`removeNone_aux_none` 📖	mathematical	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `instEquivLike`	`removeNone_aux`	—	—
`removeNone_aux_some` 📖	mathematical	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `instEquivLike`	`removeNone_aux`	—	—
`removeNone_none` 📖	mathematical	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `instEquivLike`	`removeNone`	—	`removeNone_aux_none`
`removeNone_optionCongr` 📖	mathematical	—	`removeNone` `optionCongr`	—	`ext` `Option.some_injective` `removeNone_some`
`removeNone_some` 📖	mathematical	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `instEquivLike`	`removeNone`	—	`removeNone_aux_some`
`removeNone_symm` 📖	mathematical	—	`symm` `removeNone`	—	—
`some_removeNone_iff` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `instEquivLike` `removeNone` `symm`	—	`removeNone_none` `symm_apply_apply` `removeNone_some` `EquivLike.toEmbeddingLike`

---

← Back to Index