Commit 2023-02-18 13:17 c22f5070

View on Github →

feat: port Data.Pfunctor.Univariate.M (#1834)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/PFunctor/Univariate/M.lean

added inductive PFunctor.Approx.Agree

added def PFunctor.Approx.AllAgree

added inductive PFunctor.Approx.CofixA

added theorem PFunctor.Approx.P_corec

added def PFunctor.Approx.Path

added theorem PFunctor.Approx.agree_children

added theorem PFunctor.Approx.agree_trival

added theorem PFunctor.Approx.approx_eta

added def PFunctor.Approx.children'

added theorem PFunctor.Approx.cofixA_eq_zero

added def PFunctor.Approx.head'

added theorem PFunctor.Approx.head_succ'

added def PFunctor.Approx.sCorec

added def PFunctor.Approx.truncate

added theorem PFunctor.Approx.truncate_eq_of_agree

added inductive PFunctor.M.Agree'

added structure PFunctor.M.IsBisimulation

added inductive PFunctor.M.IsPath

added theorem PFunctor.M.agree'_refl

added theorem PFunctor.M.agree_iff_agree'

added theorem PFunctor.M.approx_mk

added theorem PFunctor.M.bisim'

added theorem PFunctor.M.bisim

added theorem PFunctor.M.bisim_equiv

added theorem PFunctor.M.casesOn_mk'

added theorem PFunctor.M.casesOn_mk

added theorem PFunctor.M.cases_mk

added def PFunctor.M.children

added theorem PFunctor.M.children_mk

added def PFunctor.M.corec'

added def PFunctor.M.corecOn

added theorem PFunctor.M.corec_def

added theorem PFunctor.M.corec_unique

added def PFunctor.M.corec₁

added theorem PFunctor.M.default_consistent

added def PFunctor.M.dest

added theorem PFunctor.M.dest_corec

added theorem PFunctor.M.dest_mk

added theorem PFunctor.M.eq_of_bisim

added theorem PFunctor.M.ext'

added theorem PFunctor.M.ext

added theorem PFunctor.M.ext_aux

added theorem PFunctor.M.head'_eq_head

added def PFunctor.M.head

added theorem PFunctor.M.head_eq_head'

added theorem PFunctor.M.head_mk

added theorem PFunctor.M.head_succ

added def PFunctor.M.ichildren

added theorem PFunctor.M.ichildren_mk

added theorem PFunctor.M.isPath_cons'

added theorem PFunctor.M.isPath_cons

added def PFunctor.M.iselect

added theorem PFunctor.M.iselect_cons

added theorem PFunctor.M.iselect_eq_default

added theorem PFunctor.M.iselect_nil

added def PFunctor.M.isubtree

added theorem PFunctor.M.isubtree_cons

added theorem PFunctor.M.mk_dest

added theorem PFunctor.M.mk_inj

added theorem PFunctor.M.nth_of_bisim

added theorem PFunctor.M.truncate_approx

added def PFunctor.M

added structure PFunctor.MIntl