Basic

📁 Source: Mathlib/Data/QPF/Univariate/Basic.lean

Statistics

Metric	Count
Definitions QPF, corec, dest, dest, mk, rec, IsPrecongr, IsUniform, LiftpPreservation, Mcongr, P, SuppPreservation, Wequiv, Wrepr, Wsetoid, abs, comp, corecF, fixToW, instInhabitedCofixOfAP, quotientQPF, recF, repr, toFunctor	24
Theorems bisim, bisim', bisim_rel, dest_corec, dest_mk, ind, ind_aux, ind_rec, mk_dest, rec_eq, rec_unique, abs', refl, Wrepr_equiv, abs_map, abs_repr, comp_map, corecF_eq, has_good_supp_iff, id_map, lawfulFunctor, liftpPreservation_iff_uniform, liftp_iff, liftp_iff', liftp_iff_of_isUniform, liftr_iff, mem_supp, recF_eq, recF_eq', recF_eq_of_Wequiv, suppPreservation_iff_liftpPreservation, suppPreservation_iff_uniform, supp_eq, supp_eq_of_isUniform, supp_map	35
Total	59

QPF

Definitions

Name	Category	Theorems
IsPrecongr 📖	MathDef	—
IsUniform 📖	MathDef	2 math math: suppPreservation_iff_uniform, liftpPreservation_iff_uniform
LiftpPreservation 📖	MathDef	2 math math: suppPreservation_iff_liftpPreservation, liftpPreservation_iff_uniform
Mcongr 📖	MathDef	—
P 📖	CompOp	11 math math: liftp_iff', recF_eq', Fix.ind_aux, abs_map, corecF_eq, mem_supp, recF_eq, has_good_supp_iff, liftr_iff, supp_eq_of_isUniform, liftp_iff
SuppPreservation 📖	MathDef	2 math math: suppPreservation_iff_uniform, suppPreservation_iff_liftpPreservation
Wequiv 📖	CompData	3 math math: Wequiv.abs', Wrepr_equiv, Wequiv.refl
Wrepr 📖	CompOp	1 math math: Wrepr_equiv
Wsetoid 📖	CompOp	1 math math: Fix.ind_aux
abs 📖	CompOp	10 math math: liftp_iff', abs_repr, recF_eq', Fix.ind_aux, abs_map, recF_eq, has_good_supp_iff, liftr_iff, supp_eq_of_isUniform, liftp_iff
comp 📖	CompOp	—
corecF 📖	CompOp	1 math math: corecF_eq
fixToW 📖	CompOp	—
instInhabitedCofixOfAP 📖	CompOp	—
quotientQPF 📖	CompOp	—
recF 📖	CompOp	3 math math: recF_eq', recF_eq, recF_eq_of_Wequiv
repr 📖	CompOp	2 math math: abs_repr, corecF_eq
toFunctor 📖	CompOp	14 math math: liftp_iff', liftp_iff_of_isUniform, abs_map, Cofix.dest_corec, Fix.rec_eq, supp_eq, comp_map, supp_map, id_map, mem_supp, has_good_supp_iff, liftr_iff, supp_eq_of_isUniform, liftp_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
Wrepr_equiv 📖	mathematical	—	Wequiv Wrepr	—	Wequiv.abs' abs_repr
abs_map 📖	mathematical	—	abs PFunctor.map P toFunctor	—	—
abs_repr 📖	mathematical	—	abs repr	—	—
comp_map 📖	mathematical	—	toFunctor	—	abs_repr abs_map
corecF_eq 📖	mathematical	—	PFunctor.M.dest P corecF PFunctor.map PFunctor.M repr	—	corecF.eq_1
has_good_supp_iff 📖	mathematical	—	Functor.Liftp toFunctor abs PFunctor.A P Set Set.instHasSubset Set.image PFunctor.B Set.univ	—	liftp_iff mem_supp Set.mem_image_of_mem Set.mem_univ
id_map 📖	mathematical	—	toFunctor	—	abs_repr abs_map
lawfulFunctor 📖	—	toFunctor	—	—	id_map comp_map
liftpPreservation_iff_uniform 📖	mathematical	—	LiftpPreservation IsUniform	—	suppPreservation_iff_liftpPreservation suppPreservation_iff_uniform
liftp_iff 📖	mathematical	—	Functor.Liftp toFunctor abs PFunctor.A P	—	abs_repr abs_map
liftp_iff' 📖	mathematical	—	Functor.Liftp toFunctor abs PFunctor.A P	—	abs_repr abs_map
liftp_iff_of_isUniform 📖	mathematical	IsUniform	Functor.Liftp toFunctor	—	liftp_iff abs_repr supp_eq_of_isUniform Set.mem_univ
liftr_iff 📖	mathematical	—	Functor.Liftr toFunctor abs PFunctor.A P	—	abs_repr abs_map
mem_supp 📖	mathematical	—	Set Set.instMembership Functor.supp toFunctor Set.image PFunctor.B P Set.univ	—	Functor.supp.eq_1 liftp_iff Set.mem_image_of_mem Set.mem_univ
recF_eq 📖	mathematical	—	recF abs PFunctor.map P PFunctor.W PFunctor.W.dest	—	—
recF_eq' 📖	mathematical	—	recF PFunctor.A P PFunctor.B abs PFunctor.map PFunctor.W	—	—
recF_eq_of_Wequiv 📖	mathematical	Wequiv	recF	—	abs_map
suppPreservation_iff_liftpPreservation 📖	mathematical	—	SuppPreservation LiftpPreservation	—	liftp_iff_of_isUniform suppPreservation_iff_uniform supp_eq_of_isUniform PFunctor.liftp_iff' Set.image_univ
suppPreservation_iff_uniform 📖	mathematical	—	SuppPreservation IsUniform	—	PFunctor.supp_eq supp_eq_of_isUniform
supp_eq 📖	mathematical	—	Functor.supp toFunctor setOf	—	Set.ext mem_supp
supp_eq_of_isUniform 📖	mathematical	IsUniform	Functor.supp toFunctor abs PFunctor.A P Set.image PFunctor.B Set.univ	—	Set.ext mem_supp
supp_map 📖	mathematical	IsUniform	Functor.supp toFunctor Set.image	—	abs_repr abs_map PFunctor.map_eq supp_eq_of_isUniform Set.image_comp

QPF.Cofix

Definitions

Name	Category	Theorems
corec 📖	CompOp	—
dest 📖	CompOp	1 math math: dest_corec

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bisim 📖	—	Functor.Liftr QPF.toFunctor QPF.Cofix dest	—	—	bisim_rel QPF.liftr_iff QPF.abs_map PFunctor.map_eq
bisim' 📖	—	dest QPF.abs QPF.Cofix PFunctor.A QPF.P	—	—	bisim QPF.liftr_iff
bisim_rel 📖	—	QPF.toFunctor QPF.Cofix dest	—	—	Quot.factor_mk_eq QPF.comp_map
dest_corec 📖	mathematical	—	dest QPF.toFunctor QPF.Cofix	—	dest.eq_1 corec.eq_1 QPF.corecF_eq QPF.abs_map QPF.abs_repr QPF.comp_map

QPF.Fix

Definitions

Name	Category	Theorems
dest 📖	CompOp	2 math math: mk_dest, dest_mk
mk 📖	CompOp	—
rec 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dest_mk 📖	mathematical	—	dest	—	rec_eq dest.eq_1 QPF.comp_map QPF.id_map mk_dest
ind 📖	—	—	—	—	ind_aux QPF.liftp_iff
ind_aux 📖	mathematical	—	QPF.abs QPF.Fix PFunctor.A QPF.P PFunctor.W QPF.Wsetoid PFunctor.B	—	QPF.Wequiv.abs' QPF.abs_map QPF.abs_repr PFunctor.map_eq QPF.recF_eq QPF.Wrepr_equiv
ind_rec 📖	—	—	—	—	ind_aux QPF.abs_map PFunctor.map_eq
mk_dest 📖	mathematical	—	dest	—	dest.eq_1 rec_eq QPF.id_map QPF.comp_map
rec_eq 📖	mathematical	—	QPF.toFunctor QPF.Fix	—	QPF.recF_eq_of_Wequiv QPF.fixToW.eq_1 QPF.Wrepr_equiv PFunctor.map_eq QPF.recF_eq PFunctor.map_map QPF.abs_map QPF.abs_repr
rec_unique 📖	—	QPF.toFunctor QPF.Fix	—	—	rec_eq

QPF.Wequiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
abs' 📖	mathematical	QPF.abs PFunctor.W QPF.P PFunctor.W.dest	QPF.Wequiv	—	—
refl 📖	mathematical	—	QPF.Wequiv	—	—

(root)

Definitions

Name	Category	Theorems
QPF 📖	CompData	—

---

← Back to Index