Commit 2023-10-09 08:36 196e587a

View on Github →

style: Qpf to QPF & PFunctor.IdxCat to PFunctor.Idx (#7499) IdxCat was a mathport-ism caused by the name being capitalized in Lean 3.

Estimated changes

added def PFunctor.Idx
deleted def PFunctor.IdxCat
modified def PFunctor.Obj.iget
modified def PFunctor.M.ichildren
modified theorem PFunctor.M.ichildren_mk
added theorem QPF.Cofix.bisim'
added theorem QPF.Cofix.bisim
added theorem QPF.Cofix.bisim_rel
added def QPF.Cofix.corec
added def QPF.Cofix.dest
added theorem QPF.Cofix.dest_corec
added def QPF.Cofix
added def QPF.Fix.dest
added theorem QPF.Fix.dest_mk
added theorem QPF.Fix.ind
added theorem QPF.Fix.ind_aux
added theorem QPF.Fix.ind_rec
added def QPF.Fix.mk
added theorem QPF.Fix.mk_dest
added def QPF.Fix.rec
added theorem QPF.Fix.rec_eq
added theorem QPF.Fix.rec_unique
added def QPF.Fix
added def QPF.IsPrecongr
added def QPF.IsUniform
added def QPF.Mcongr
added theorem QPF.Wequiv.abs'
added theorem QPF.Wequiv.refl
added theorem QPF.Wequiv.symm
added inductive QPF.Wequiv
added def QPF.Wrepr
added theorem QPF.Wrepr_equiv
added def QPF.Wsetoid
added def QPF.comp
added theorem QPF.comp_map
added def QPF.corecF
added theorem QPF.corecF_eq
added def QPF.fixToW
added theorem QPF.has_good_supp_iff
added theorem QPF.id_map
added theorem QPF.lawfulFunctor
added theorem QPF.liftp_iff'
added theorem QPF.liftp_iff
added theorem QPF.liftr_iff
added theorem QPF.mem_supp
added def QPF.quotientQPF
added def QPF.recF
added theorem QPF.recF_eq'
added theorem QPF.recF_eq
added theorem QPF.recF_eq_of_Wequiv
added theorem QPF.supp_eq
added theorem QPF.supp_map
deleted theorem Qpf.Cofix.bisim'
deleted theorem Qpf.Cofix.bisim
deleted theorem Qpf.Cofix.bisim_rel
deleted def Qpf.Cofix.corec
deleted def Qpf.Cofix.dest
deleted theorem Qpf.Cofix.dest_corec
deleted def Qpf.Cofix
deleted def Qpf.Fix.dest
deleted theorem Qpf.Fix.dest_mk
deleted theorem Qpf.Fix.ind
deleted theorem Qpf.Fix.ind_aux
deleted theorem Qpf.Fix.ind_rec
deleted def Qpf.Fix.mk
deleted theorem Qpf.Fix.mk_dest
deleted def Qpf.Fix.rec
deleted theorem Qpf.Fix.rec_eq
deleted theorem Qpf.Fix.rec_unique
deleted def Qpf.Fix
deleted def Qpf.IsPrecongr
deleted def Qpf.IsUniform
deleted def Qpf.Mcongr
deleted theorem Qpf.Wequiv.abs'
deleted theorem Qpf.Wequiv.refl
deleted theorem Qpf.Wequiv.symm
deleted inductive Qpf.Wequiv
deleted def Qpf.Wrepr
deleted theorem Qpf.Wrepr_equiv
deleted def Qpf.Wsetoid
deleted def Qpf.comp
deleted theorem Qpf.comp_map
deleted def Qpf.corecF
deleted theorem Qpf.corecF_eq
deleted def Qpf.fixToW
deleted theorem Qpf.has_good_supp_iff
deleted theorem Qpf.id_map
deleted theorem Qpf.lawfulFunctor
deleted theorem Qpf.liftp_iff'
deleted theorem Qpf.liftp_iff
deleted theorem Qpf.liftr_iff
deleted theorem Qpf.mem_supp
deleted def Qpf.quotientQpf
deleted def Qpf.recF
deleted theorem Qpf.recF_eq'
deleted theorem Qpf.recF_eq
deleted theorem Qpf.recF_eq_of_Wequiv
deleted theorem Qpf.supp_eq
deleted theorem Qpf.supp_eq_of_isUniform
deleted theorem Qpf.supp_map