Bifunctor

📁 Source: Mathlib/Control/Bifunctor.lean

Statistics

Metric	Count
Definitions Bifunctor, bimap, const, flip, fst, functor, snd, bifunctor, bifunctor, LawfulBifunctor, bifunctor, bifunctor	12
Theorems comp_fst, comp_snd, fst_comp_fst, fst_comp_snd, fst_id, fst_snd, id_fst, id_snd, lawfulFunctor, snd_comp_fst, snd_comp_snd, snd_fst, snd_id, lawfulBifunctor, lawfulBifunctor, bimap_bimap, bimap_comp_bimap, bimap_id_id, const, flip, id_bimap, lawfulBifunctor, lawfulBifunctor	23
Total	35

Bifunctor

Definitions

Name	Category	Theorems
bimap 📖	CompOp	12 math math: LawfulBifunctor.bimap_comp_bimap, LawfulBitraversable.bitraverse_eq_bimap_id, mapEquiv_apply, mapEquiv_symm_apply, LawfulBifunctor.id_bimap, fst_comp_snd, LawfulBitraversable.bitraverse_eq_bimap_id', LawfulBifunctor.bimap_id_id, snd_fst, snd_comp_fst, fst_snd, LawfulBifunctor.bimap_bimap
const 📖	CompOp	1 math math: LawfulBifunctor.const
flip 📖	CompOp	1 math math: LawfulBifunctor.flip
fst 📖	CompOp	10 math math: fst_id, id_fst, fst_comp_fst, comp_fst, Bitraversable.tfst_eq_fst_id, fst_comp_snd, snd_fst, snd_comp_fst, Bitraversable.tfst_eq_fst_id', fst_snd
functor 📖	CompOp	1 math math: lawfulFunctor
snd 📖	CompOp	10 math math: id_snd, comp_snd, snd_comp_snd, Bitraversable.tsnd_eq_snd_id', Bitraversable.tsnd_eq_snd_id, fst_comp_snd, snd_fst, snd_comp_fst, snd_id, fst_snd

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_fst 📖	mathematical	—	fst	—	LawfulBifunctor.bimap_bimap
comp_snd 📖	mathematical	—	snd	—	LawfulBifunctor.bimap_bimap
fst_comp_fst 📖	mathematical	—	fst	—	comp_fst
fst_comp_snd 📖	mathematical	—	fst snd bimap	—	fst_snd
fst_id 📖	mathematical	—	fst	—	id_fst
fst_snd 📖	mathematical	—	fst snd bimap	—	LawfulBifunctor.bimap_bimap
id_fst 📖	mathematical	—	fst	—	LawfulBifunctor.id_bimap
id_snd 📖	mathematical	—	snd	—	LawfulBifunctor.id_bimap
lawfulFunctor 📖	mathematical	—	functor	—	LawfulBifunctor.bimap_id_id LawfulBifunctor.bimap_bimap
snd_comp_fst 📖	mathematical	—	snd fst bimap	—	snd_fst
snd_comp_snd 📖	mathematical	—	snd	—	comp_snd
snd_fst 📖	mathematical	—	snd fst bimap	—	LawfulBifunctor.bimap_bimap
snd_id 📖	mathematical	—	snd	—	id_snd

Function.bicompl

Definitions

Name	Category	Theorems
bifunctor 📖	CompOp	1 math math: lawfulBifunctor

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
lawfulBifunctor 📖	mathematical	—	LawfulBifunctor Function.bicompl bifunctor	—	Functor.map_id LawfulBifunctor.bimap_id_id LawfulBifunctor.bimap_bimap Functor.map_comp_map

Function.bicompr

Definitions

Name	Category	Theorems
bifunctor 📖	CompOp	1 math math: lawfulBifunctor

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
lawfulBifunctor 📖	mathematical	—	LawfulBifunctor Function.bicompr bifunctor	—	LawfulBifunctor.bimap_id_id LawfulBifunctor.bimap_bimap

LawfulBifunctor

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bimap_bimap 📖	mathematical	—	Bifunctor.bimap	—	—
bimap_comp_bimap 📖	mathematical	—	Bifunctor.bimap	—	bimap_bimap
bimap_id_id 📖	mathematical	—	Bifunctor.bimap	—	id_bimap
const 📖	mathematical	—	LawfulBifunctor Functor.Const Bifunctor.const	—	—
flip 📖	mathematical	—	LawfulBifunctor Bifunctor.flip	—	bimap_id_id bimap_bimap
id_bimap 📖	mathematical	—	Bifunctor.bimap	—	—

Prod

Definitions

Name	Category	Theorems
bifunctor 📖	CompOp	1 math math: lawfulBifunctor

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
lawfulBifunctor 📖	mathematical	—	LawfulBifunctor bifunctor	—	—

Sum

Definitions

Name	Category	Theorems
bifunctor 📖	CompOp	1 math math: lawfulBifunctor

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
lawfulBifunctor 📖	mathematical	—	LawfulBifunctor bifunctor	—	—

(root)

Definitions

Name	Category	Theorems
Bifunctor 📖	CompData	—
LawfulBifunctor 📖	CompData	7 math math: Prod.lawfulBifunctor, Sum.lawfulBifunctor, LawfulBifunctor.flip, LawfulBitraversable.toLawfulBifunctor, Function.bicompl.lawfulBifunctor, Function.bicompr.lawfulBifunctor, LawfulBifunctor.const

---

← Back to Index