FinFun
📁 Source: Cslib/Foundations/Data/FinFun.lean
Statistics
| Metric | Count |
|---|---|
| 7 | |
| 16 | |
| Total | 23 |
Cslib
Definitions
| Name | Category | Theorems |
|---|---|---|
FinFun 📖 | CompData |
Cslib.FinFun
Definitions
| Name | Category | Theorems |
|---|---|---|
fn 📖 | CompOp | |
fromFun 📖 | CompOp | 7 mathmath:fromFun_support, fromFun_inter, fromFun_eq, fromFun_idem, fromFun_fn, coe_fromFun_id, fromFun_comm |
instFunLike 📖 | CompOp | 9 mathmath:coe_fn, fromFun_inter, fromFun_eq, fromFun_idem, coe_fromFun_id, fromFun_comm, congrFinFun, not_mem_support_zero, coe_eq_fn |
support 📖 | CompOp | |
«term_→₀_» 📖 | CompOp | — |
«term_↾₀_» 📖 | CompOp | — |
Theorems
| Name | Kind | Assumes | Proves | Validates | Depends On |
|---|---|---|---|---|---|
coe_eq_fn 📖 | mathematical | — | Cslib.FinFuninstFunLikefn | — | — |
coe_fn 📖 | mathematical | — | Cslib.FinFuninstFunLikefn | — | — |
coe_fromFun_id 📖 | mathematical | — | fromFunCslib.FinFuninstFunLikesupport | — | — |
congrFinFun 📖 | mathematical | — | Cslib.FinFuninstFunLike | — | — |
eq_fields_eq 📖 | mathematical | — | fnsupport | — | — |
ext 📖 | — | Cslib.FinFuninstFunLike | — | — | — |
fn_eq_eq 📖 | — | fn | — | — | ext |
fromFun_comm 📖 | mathematical | — | fromFunCslib.FinFuninstFunLike | — | — |
fromFun_eq 📖 | mathematical | — | Cslib.FinFuninstFunLikefromFun | — | — |
fromFun_fn 📖 | mathematical | — | fnfromFun | — | — |
fromFun_idem 📖 | mathematical | — | fromFunCslib.FinFuninstFunLike | — | — |
fromFun_inter 📖 | mathematical | — | fromFunCslib.FinFuninstFunLike | — | — |
fromFun_support 📖 | mathematical | — | supportfromFun | — | — |
mem_support_fn 📖 | mathematical | — | support | — | — |
mem_support_not_zero 📖 | mathematical | — | support | — | — |
not_mem_support_zero 📖 | mathematical | — | supportCslib.FinFuninstFunLike | — | — |
---