M

📁 Source: Mathlib/Data/PFunctor/Univariate/M.lean

Statistics

Metric	Count
Definitions M, M, M, M, M, M, M, M, M, M, Agree, AllAgree, CofixA, default, inhabited, children', head', instInhabitedCofixAOfA, sCorec, truncate, M, Agree', sMk, IsBisimulation, IsPath, casesOn, casesOn', children, corec, corec', corecOn, corec₁, dest, head, ichildren, inhabited, iselect, isubtree, mk, MIntl, approx, inhabited, M	43
Theorems instSubsingleton, P_corec, agree_children, agree_trivial, approx_eta, cofixA_eq_zero, head_succ', truncate_eq_of_agree, P_mk, head, tail, agree'_refl, agree_iff_agree', approx_mk, bisim, bisim', bisim_equiv, casesOn_mk, casesOn_mk', cases_mk, children_mk, corec_def, corec_unique, default_consistent, dest_corec, dest_mk, eq_of_bisim, ext, ext', ext_aux, head'_eq_head, head_eq_head', head_mk, head_succ, ichildren_mk, isPath_cons, isPath_cons', iselect_cons, iselect_eq_default, iselect_nil, isubtree_cons, mk_dest, mk_inj, nth_of_bisim, truncate_approx, consistent	46
Total	89

AddCommMonCat.FilteredColimits

Definitions

Name	Category	Theorems
M 📖	CompOp	—

AddMonCat.FilteredColimits

Definitions

Name	Category	Theorems
M 📖	CompOp	3 math math: colimit_add_mk_eq, colimit_zero_eq, colimit_add_mk_eq'

CommMonCat.FilteredColimits

Definitions

Name	Category	Theorems
M 📖	CompOp	—

CoxeterMatrix

Definitions

Name	Category	Theorems
M 📖	CompOp	7 math math: CoxeterSystem.simple_mul_simple_pow, isSymm, CoxeterSystem.simple_mul_simple_pow', diagonal, reindex_apply, ext_iff, symmetric

Mathlib.Tactic.Abel

Definitions

Name	Category	Theorems
M 📖	CompOp	—

Mathlib.Tactic.DepRewrite

Definitions

Name	Category	Theorems
M 📖	CompOp	—

Mathlib.Tactic.TermCongr

Definitions

Name	Category	Theorems
M 📖	CompOp	—

ModuleCat.FilteredColimits

Definitions

Name	Category	Theorems
M 📖	CompOp	4 math math: colimit_smul_mk_eq, colimit_zero_eq, colimit_add_mk_eq', colimit_add_mk_eq

MonCat.FilteredColimits

Definitions

Name	Category	Theorems
M 📖	CompOp	3 math math: colimit_mul_mk_eq', colimit_one_eq, colimit_mul_mk_eq

MvPFunctor

Definitions

Name	Category	Theorems
M 📖	CompOp	5 math math: M.dest_map, M.dest_corec, M.dest_corec', MvQPF.Cofix.abs_repr, MvQPF.corecF_eq

PFunctor

Definitions

Name	Category	Theorems
M 📖	CompOp	5 math math: M.ichildren_mk, QPF.corecF_eq, M.iselect_eq_default, M.corec_def, M.dest_corec
MIntl 📖	CompData	—

PFunctor.Approx

Definitions

Name	Category	Theorems
Agree 📖	CompData	4 math math: P_corec, PFunctor.M.agree_iff_agree', agree_trivial, PFunctor.M.default_consistent
AllAgree 📖	MathDef	2 math math: PFunctor.M.Approx.P_mk, PFunctor.MIntl.consistent
CofixA 📖	CompData	2 math math: CofixA.instSubsingleton, PFunctor.M.default_consistent
children' 📖	CompOp	2 math math: agree_children, approx_eta
head' 📖	CompOp	5 math math: PFunctor.M.head_eq_head', PFunctor.M.head'_eq_head, head_succ', PFunctor.M.head_succ, approx_eta
instInhabitedCofixAOfA 📖	CompOp	1 math math: PFunctor.M.default_consistent
sCorec 📖	CompOp	—
truncate 📖	CompOp	2 math math: PFunctor.M.truncate_approx, truncate_eq_of_agree

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
P_corec 📖	mathematical	—	Agree	—	—
agree_children 📖	mathematical	PFunctor.B head' Agree	children'	—	—
agree_trivial 📖	mathematical	—	Agree	—	—
approx_eta 📖	mathematical	—	CofixA.intro head' children'	—	—
cofixA_eq_zero 📖	—	—	—	—	—
head_succ' 📖	mathematical	AllAgree	head'	—	—
truncate_eq_of_agree 📖	mathematical	Agree	truncate	—	—

PFunctor.Approx.CofixA

Definitions

Name	Category	Theorems
default 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instSubsingleton 📖	mathematical	—	PFunctor.Approx.CofixA	—	—

PFunctor.Approx.Path

Definitions

Name	Category	Theorems
inhabited 📖	CompOp	—

PFunctor.M

Definitions

Name	Category	Theorems
Agree' 📖	CompData	2 math math: agree_iff_agree', agree'_refl
IsBisimulation 📖	CompData	—
IsPath 📖	CompData	—
casesOn 📖	CompOp	—
casesOn' 📖	CompOp	1 math math: casesOn_mk'
children 📖	CompOp	1 math math: children_mk
corec 📖	CompOp	—
corec' 📖	CompOp	—
corecOn 📖	CompOp	—
corec₁ 📖	CompOp	—
dest 📖	CompOp	4 math math: dest_mk, QPF.corecF_eq, dest_corec, mk_dest
head 📖	CompOp	5 math math: head_mk, head_eq_head', head'_eq_head, iselect_eq_default, children_mk
ichildren 📖	CompOp	1 math math: ichildren_mk
inhabited 📖	CompOp	—
iselect 📖	CompOp	4 math math: iselect_nil, iselect_eq_default, iselect_cons, nth_of_bisim
isubtree 📖	CompOp	2 math math: isubtree_cons, nth_of_bisim
mk 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
agree'_refl 📖	mathematical	—	Agree'	—	—
agree_iff_agree' 📖	mathematical	—	PFunctor.Approx.Agree PFunctor.MIntl.approx Agree'	—	—
approx_mk 📖	mathematical	—	PFunctor.MIntl.approx PFunctor.A PFunctor.Approx.CofixA.intro	—	—
bisim 📖	—	dest PFunctor.A	—	—	eq_of_bisim
bisim' 📖	—	dest PFunctor.A	—	—	bisim
bisim_equiv 📖	—	dest PFunctor.A	—	—	bisim'
casesOn_mk 📖	—	—	—	—	—
casesOn_mk' 📖	mathematical	—	casesOn' PFunctor.A	—	—
cases_mk 📖	mathematical	—	cases	—	—
children_mk 📖	mathematical	—	children PFunctor.A PFunctor.B head	—	ext'
corec_def 📖	mathematical	—	PFunctor.map PFunctor.M	—	—
corec_unique 📖	—	dest PFunctor.map PFunctor.M	—	—	bisim' PFunctor.map_eq
default_consistent 📖	mathematical	—	PFunctor.Approx.Agree PFunctor.Approx.CofixA PFunctor.Approx.instInhabitedCofixAOfA	—	—
dest_corec 📖	mathematical	—	dest PFunctor.map PFunctor.M	—	corec_def
dest_mk 📖	mathematical	—	dest	—	—
eq_of_bisim 📖	—	IsBisimulation	—	—	ext nth_of_bisim iselect_eq_default
ext 📖	—	iselect	—	—	ext' PFunctor.Approx.CofixA.instSubsingleton ext_aux agree_iff_agree' PFunctor.MIntl.consistent
ext' 📖	—	PFunctor.MIntl.approx	—	—	—
ext_aux 📖	mathematical	Agree' iselect	PFunctor.MIntl.approx	—	PFunctor.Approx.CofixA.instSubsingleton iselect_cons
head'_eq_head 📖	mathematical	—	PFunctor.Approx.head' PFunctor.MIntl.approx head	—	PFunctor.Approx.head_succ'
head_eq_head' 📖	mathematical	—	head PFunctor.Approx.head' PFunctor.MIntl.approx	—	PFunctor.Approx.head_succ'
head_mk 📖	mathematical	—	head PFunctor.A	—	—
head_succ 📖	mathematical	—	PFunctor.Approx.head' PFunctor.MIntl.approx	—	PFunctor.Approx.head_succ' PFunctor.MIntl.consistent
ichildren_mk 📖	mathematical	—	ichildren PFunctor.Obj.iget PFunctor.M	—	—
isPath_cons 📖	—	IsPath PFunctor.Idx PFunctor.A PFunctor.B	—	—	—
isPath_cons' 📖	—	IsPath PFunctor.Idx PFunctor.A PFunctor.B	—	—	—
iselect_cons 📖	mathematical	—	iselect PFunctor.Idx PFunctor.A PFunctor.B	—	isubtree_cons
iselect_eq_default 📖	mathematical	IsPath	iselect head PFunctor.M	—	casesOn_mk'
iselect_nil 📖	mathematical	—	iselect PFunctor.Idx PFunctor.A	—	—
isubtree_cons 📖	mathematical	—	isubtree PFunctor.Idx PFunctor.A PFunctor.B	—	casesOn_mk'
mk_dest 📖	mathematical	—	dest	—	ext' PFunctor.Approx.CofixA.instSubsingleton PFunctor.Approx.head_succ' PFunctor.MIntl.consistent PFunctor.Approx.head'.eq_1
mk_inj 📖	—	—	—	—	—
nth_of_bisim 📖	mathematical	IsBisimulation IsPath	iselect isubtree PFunctor.A	—	IsBisimulation.tail isubtree_cons isPath_cons' IsBisimulation.head isPath_cons
truncate_approx 📖	mathematical	—	PFunctor.Approx.truncate PFunctor.MIntl.approx	—	PFunctor.Approx.truncate_eq_of_agree PFunctor.MIntl.consistent

PFunctor.M.Approx

Definitions

Name	Category	Theorems
sMk 📖	CompOp	1 math math: P_mk

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
P_mk 📖	mathematical	—	PFunctor.Approx.AllAgree sMk	—	PFunctor.MIntl.consistent

PFunctor.M.IsBisimulation

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
head 📖	—	PFunctor.M.IsBisimulation PFunctor.A	—	—	—
tail 📖	—	PFunctor.M.IsBisimulation PFunctor.A	—	—	—

PFunctor.MIntl

Definitions

Name	Category	Theorems
approx 📖	CompOp	8 math math: PFunctor.M.head_eq_head', PFunctor.M.truncate_approx, PFunctor.M.head'_eq_head, consistent, PFunctor.M.agree_iff_agree', PFunctor.M.approx_mk, PFunctor.M.ext_aux, PFunctor.M.head_succ
inhabited 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
consistent 📖	mathematical	—	PFunctor.Approx.AllAgree approx	—	—

SingularManifold

Definitions

Name	Category	Theorems
M 📖	CompOp	14 math math: empty_M, instIsEmptyMEmpty, isManifold, sum_f, boundaryless, instCompactSpaceM, instBoundarylessManifoldRealM, compactSpace, map_f, map_comp, hf, map_M, instIsManifoldRealM, sum_M

---

← Back to Index