OfFn

📁 Source: Mathlib/Data/List/OfFn.lean

Statistics

Metric	Count
Definitions `equivSigmaTuple`, `ofFnRec`	2
Theorems `equivSigmaTuple_apply_fst`, `equivSigmaTuple_apply_snd`, `equivSigmaTuple_symm_apply`, `exists_iff_exists_tuple`, `find?_ofFn_eq_some`, `find?_ofFn_eq_some_of_injective`, `forall_iff_forall_tuple`, `forall_mem_ofFn_iff`, `getLast_ofFn_succ`, `get_ofFn`, `map_ofFn`, `mem_ofFn'`, `ofFnRec_ofFn`, `ofFn_comp'`, `ofFn_congr`, `ofFn_cons`, `ofFn_const`, `ofFn_fin_append`, `ofFn_fin_repeat`, `ofFn_get`, `ofFn_getElem`, `ofFn_getElem_eq_map`, `ofFn_inj`, `ofFn_inj'`, `ofFn_injective`, `ofFn_mul`, `ofFn_mul'`, `ofFn_succ'`, `pairwise_ofFn`, `sorted_ofFn_iff`	30
Total	32

List

Definitions

Name	Category	Theorems
`equivSigmaTuple` 📖	CompOp	3 math math: `equivSigmaTuple_symm_apply`, `equivSigmaTuple_apply_snd`, `equivSigmaTuple_apply_fst`
`ofFnRec` 📖	CompOp	1 math math: `ofFnRec_ofFn`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`equivSigmaTuple_apply_fst` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `equivSigmaTuple`	—	—
`equivSigmaTuple_apply_snd` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `equivSigmaTuple`	—	—
`equivSigmaTuple_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `equivSigmaTuple`	—	—
`exists_iff_exists_tuple` 📖	—	—	—	—	`Function.Surjective.exists` `Equiv.surjective` `Sigma.exists`
`find?_ofFn_eq_some` 📖	—	—	—	—	—
`find?_ofFn_eq_some_of_injective` 📖	—	—	—	—	—
`forall_iff_forall_tuple` 📖	—	—	—	—	`Function.Surjective.forall` `Equiv.surjective` `Sigma.forall`
`forall_mem_ofFn_iff` 📖	—	—	—	—	—
`getLast_ofFn_succ` 📖	—	—	—	—	—
`get_ofFn` 📖	—	—	—	—	—
`map_ofFn` 📖	—	—	—	—	—
`mem_ofFn'` 📖	mathematical	—	`Set` `Set.instMembership` `Set.range`	—	—
`ofFnRec_ofFn` 📖	mathematical	—	`ofFnRec`	—	`Function.LeftInverse.cast_eq` `Equiv.rightInverse_symm`
`ofFn_comp'` 📖	—	—	—	—	`map_ofFn`
`ofFn_congr` 📖	—	—	—	—	—
`ofFn_cons` 📖	mathematical	—	`Fin.cons`	—	—
`ofFn_const` 📖	—	—	—	—	—
`ofFn_fin_append` 📖	mathematical	—	`Fin.append`	—	`Fin.append_left'` `Fin.append_right`
`ofFn_fin_repeat` 📖	mathematical	—	`Fin.repeat`	—	`LT.lt.trans_eq` `Fin.prop` `ofFn_mul`
`ofFn_get` 📖	—	—	—	—	—
`ofFn_getElem` 📖	—	—	—	—	`ofFn_get`
`ofFn_getElem_eq_map` 📖	—	—	—	—	`map_ofFn` `ofFn_getElem`
`ofFn_inj` 📖	—	—	—	—	`ofFn_injective`
`ofFn_inj'` 📖	—	—	—	—	`Equiv.injective`
`ofFn_injective` 📖	—	—	—	—	`ofFn_inj'`
`ofFn_mul` 📖	mathematical	—	`LT.lt.trans_eq` `Fin.prop`	—	`LT.lt.trans_eq` `Fin.prop` `ofFn_congr` `ofFn_succ'`
`ofFn_mul'` 📖	mathematical	—	`LT.lt.trans_eq` `Fin.prop`	—	`LT.lt.trans_eq` `Fin.prop` `ofFn_congr` `ofFn_mul`
`ofFn_succ'` 📖	—	—	—	—	—
`pairwise_ofFn` 📖	—	—	—	—	—
`sorted_ofFn_iff` 📖	—	—	—	—	`pairwise_ofFn`

---

← Back to Index