Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-07-20 17:56 b66d1bee

View on Github →

feat(data/multivariate/qpf): definition (#3395) Part of #3317

Estimated changes

Modified src/control/functor/multivariate.lean

Created src/data/pfunctor/multivariate/basic.lean

added def mvpfunctor.append_contents

added def mvpfunctor.comp.get

added theorem mvpfunctor.comp.get_map

added theorem mvpfunctor.comp.get_mk

added def mvpfunctor.comp.mk

added theorem mvpfunctor.comp.mk_get

added def mvpfunctor.comp

added theorem mvpfunctor.comp_map

added def mvpfunctor.const.get

added theorem mvpfunctor.const.get_map

added theorem mvpfunctor.const.get_mk

added def mvpfunctor.const.mk

added theorem mvpfunctor.const.mk_get

added def mvpfunctor.const

added def mvpfunctor.drop

added theorem mvpfunctor.id_map

added def mvpfunctor.last

added theorem mvpfunctor.liftp_iff'

added theorem mvpfunctor.liftp_iff

added theorem mvpfunctor.liftr_iff

added def mvpfunctor.map

added theorem mvpfunctor.map_eq

added def mvpfunctor.obj

added theorem mvpfunctor.supp_eq

added structure mvpfunctor

Modified src/data/pfunctor/univariate/basic.lean

added def pfunctor.W.children

added def pfunctor.W.head

Created src/data/qpf/multivariate/basic.lean

added theorem mvqpf.comp_map

added theorem mvqpf.has_good_supp_iff

added def mvqpf.is_uniform

added theorem mvqpf.liftp_iff

added theorem mvqpf.liftp_iff_of_is_uniform

added def mvqpf.liftp_preservation

added theorem mvqpf.liftp_preservation_iff_uniform

added theorem mvqpf.liftr_iff

added theorem mvqpf.mem_supp

added theorem mvqpf.supp_eq

added theorem mvqpf.supp_eq_of_is_uniform

added theorem mvqpf.supp_map

added def mvqpf.supp_preservation

added theorem mvqpf.supp_preservation_iff_liftp_preservation

added theorem mvqpf.supp_preservation_iff_uniform