Basic

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

Statistics

Metric	Count
Definitions instMvQPFObj, MvQPF, IsUniform, LiftPPreservation, P, SuppPreservation, abs, ofEquiv, repr, toMvFunctor	10
Theorems abs_map, abs_repr, comp_map, has_good_supp_iff, id_map, lawfulMvFunctor, liftP_iff, liftP_iff_of_isUniform, liftR_iff, liftpPreservation_iff_uniform, mem_supp, suppPreservation_iff_isUniform, suppPreservation_iff_liftpPreservation, supp_eq, supp_eq_of_isUniform, supp_map	16
Total	26

MvPFunctor

Definitions

Name	Category	Theorems
instMvQPFObj 📖	CompOp	—

MvQPF

Definitions

Name	Category	Theorems
IsUniform 📖	MathDef	2 math math: liftpPreservation_iff_uniform, suppPreservation_iff_isUniform
LiftPPreservation 📖	MathDef	2 math math: liftpPreservation_iff_uniform, suppPreservation_iff_liftpPreservation
P 📖	CompOp	13 math math: has_good_supp_iff, Fix.ind_aux, mem_supp, recF_eq', liftR_iff, wrepr_wMk, supp_eq_of_isUniform, abs_map, Cofix.abs_repr, corecF_eq, liftP_iff, recF_eq, wEquiv_map
SuppPreservation 📖	MathDef	2 math math: suppPreservation_iff_liftpPreservation, suppPreservation_iff_isUniform
abs 📖	CompOp	10 math math: has_good_supp_iff, abs_repr, Fix.ind_aux, recF_eq', liftR_iff, wrepr_wMk, supp_eq_of_isUniform, abs_map, liftP_iff, recF_eq
ofEquiv 📖	CompOp	—
repr 📖	CompOp	3 math math: abs_repr, wrepr_wMk, corecF_eq
toMvFunctor 📖	CompOp	18 math math: supp_eq, liftR_map_last', has_good_supp_iff, comp_map, liftR_map_last, mem_supp, Cofix.dest_corec', Cofix.dest_corec, liftR_iff, lawfulMvFunctor, corec_roll, id_map, supp_eq_of_isUniform, supp_map, abs_map, liftP_iff, liftP_iff_of_isUniform, Fix.rec_eq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
abs_map 📖	mathematical	—	abs MvFunctor.map MvPFunctor.Obj P MvPFunctor.instMvFunctorObj toMvFunctor	—	—
abs_repr 📖	mathematical	—	abs repr	—	—
comp_map 📖	mathematical	—	MvFunctor.map toMvFunctor TypeVec.comp	—	abs_repr abs_map
has_good_supp_iff 📖	mathematical	—	MvFunctor.LiftP toMvFunctor abs MvPFunctor.A P TypeVec.Arrow MvPFunctor.B Set Set.instHasSubset Set.image Set.univ	—	liftP_iff mem_supp Set.mem_image_of_mem Set.mem_univ
id_map 📖	mathematical	—	MvFunctor.map toMvFunctor TypeVec.id	—	abs_repr abs_map
lawfulMvFunctor 📖	mathematical	—	LawfulMvFunctor toMvFunctor	—	id_map comp_map
liftP_iff 📖	mathematical	—	MvFunctor.LiftP toMvFunctor abs MvPFunctor.A P TypeVec.Arrow MvPFunctor.B	—	abs_repr abs_map
liftP_iff_of_isUniform 📖	mathematical	IsUniform	MvFunctor.LiftP toMvFunctor	—	liftP_iff abs_repr supp_eq_of_isUniform Set.mem_univ
liftR_iff 📖	mathematical	—	MvFunctor.LiftR toMvFunctor abs MvPFunctor.A P TypeVec.Arrow MvPFunctor.B	—	abs_repr abs_map
liftpPreservation_iff_uniform 📖	mathematical	—	LiftPPreservation IsUniform	—	suppPreservation_iff_liftpPreservation suppPreservation_iff_isUniform
mem_supp 📖	mathematical	—	Set Set.instMembership MvFunctor.supp toMvFunctor Set.image MvPFunctor.B P Set.univ	—	MvFunctor.supp.eq_1 liftP_iff Set.mem_image_of_mem Set.mem_univ
suppPreservation_iff_isUniform 📖	mathematical	—	SuppPreservation IsUniform	—	MvPFunctor.supp_eq Set.ext supp_eq_of_isUniform
suppPreservation_iff_liftpPreservation 📖	mathematical	—	SuppPreservation LiftPPreservation	—	suppPreservation_iff_isUniform supp_eq_of_isUniform Set.image_univ Set.ext
supp_eq 📖	mathematical	—	MvFunctor.supp toMvFunctor setOf	—	Set.ext mem_supp
supp_eq_of_isUniform 📖	mathematical	IsUniform	MvFunctor.supp toMvFunctor abs MvPFunctor.A P TypeVec.Arrow MvPFunctor.B Set.image Set.univ	—	Set.ext mem_supp
supp_map 📖	mathematical	IsUniform	MvFunctor.supp toMvFunctor MvFunctor.map Set.image	—	abs_repr abs_map MvPFunctor.map_eq supp_eq_of_isUniform Set.image_comp

(root)

Definitions

Name	Category	Theorems
MvQPF 📖	CompData	—

---

← Back to Index