Basic

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

Statistics

Metric	Count
Definitions DFunLike, hasCoeToFun	2
Theorems coe_eq_coe_fn, coe_fn_eq, coe_injective, coe_injective', congr_arg, congr_fun, dite_apply, exists_ne, ext, ext', ext'_iff, ext_iff, ite_apply, ne_iff, subsingleton_cod, subsingleton_dom	16
Total	18

DFunLike

Definitions

Name	Category	Theorems
hasCoeToFun 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_eq_coe_fn 📖	mathematical	—	coe	—	—
coe_fn_eq 📖	mathematical	—	coe	—	coe_injective'
coe_injective 📖	mathematical	—	coe	—	coe_injective'
coe_injective' 📖	mathematical	—	coe	—	—
congr_arg 📖	mathematical	—	coe	—	—
congr_fun 📖	mathematical	—	coe	—	—
dite_apply 📖	mathematical	—	coe	—	—
exists_ne 📖	—	—	—	—	ne_iff
ext 📖	—	coe	—	—	coe_injective'
ext' 📖	—	coe	—	—	coe_injective'
ext'_iff 📖	mathematical	—	coe	—	coe_fn_eq
ext_iff 📖	mathematical	—	coe	—	coe_fn_eq
ite_apply 📖	mathematical	—	coe	—	dite_apply
ne_iff 📖	—	—	—	—	Iff.not ext_iff
subsingleton_cod 📖	—	—	—	—	Function.Injective.subsingleton coe_injective
subsingleton_dom 📖	—	—	—	—	Function.Injective.subsingleton coe_injective Unique.instSubsingleton

(root)

Definitions

Name	Category	Theorems
DFunLike 📖	CompData	—

---

← Back to Index