Theorems · Theorem · category theory
MvQPF.abs_map
∀ {n : ℕ} {F : TypeVec.{u} n → Type u_1} [self : MvQPF F] {α β : TypeVec.{u} n} (f : α.Arrow β) (p : ↑(MvQPF.P F) α),
MvQPF.abs (MvFunctor.map f p) = MvFunctor.map f (MvQPF.abs p)- Defined in
- Mathlib.Data.QPF.Multivariate.Basic
- Cited by
- 13 results in Mathlib
- Foundations
- Depth 8 from the axioms · uses no axioms
- Assumes
- MvQPF
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- TypeVecstatement and proof · cited by 185
- TypeVec.Arrowstatement · cited by 144
- MvFunctor.mapstatement · cited by 58
- MvQPFstatement and proof · cited by 48
- MvPFunctor.Objstatement · cited by 43
- MvQPF.absstatement · cited by 31
- MvQPF.Pstatement · cited by 30
Cited by13
Results whose statement or proof uses this declaration.
- MvQPF.comp_mapproof · cited by 6
- MvQPF.liftP_iffproof · cited by 4
- MvQPF.Cofix.dest_corecproof · cited by 4
- MvQPF.Fix.rec_eqproof · cited by 3
- MvQPF.liftR_iffproof · cited by 2
- MvQPF.Cofix.bisimproof · cited by 2
- MvQPF.Fix.ind_auxproof · cited by 2
- MvQPF.Fix.ind_recproof · cited by 2
- MvQPF.recF_eq_of_wEquivproof · cited by 1
- MvQPF.supp_mapproof · cited by 0
- MvQPF.id_mapproof · cited by 0
- MvQPF.wEquiv_mapproof · cited by 0