Commit 2023-04-18 03:37 cb877dd2

View on Github →

feat: port Data.QPF.Univariate.Basic (#3470)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/QPF/Univariate/Basic.lean

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.LiftpPreservation

added def Qpf.Mcongr

added def Qpf.SuppPreservation

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.liftpPreservation_iff_uniform

added theorem Qpf.liftp_iff'

added theorem Qpf.liftp_iff

added theorem Qpf.liftp_iff_of_isUniform

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.suppPreservation_iff_liftpPreservation

added theorem Qpf.suppPreservation_iff_uniform

added theorem Qpf.supp_eq

added theorem Qpf.supp_eq_of_isUniform

added theorem Qpf.supp_map