Theorems · Inductive type · category theory
PFunctor.Approx.Agree
{F : PFunctor.{uA, uB}} → {n : ℕ} → PFunctor.Approx.CofixA F n → PFunctor.Approx.CofixA F (n + 1) → PropRelation between two approximations of the cofix of a pfunctor that state they both contain the same data until one of them is truncated
- Defined in
- Mathlib.Data.PFunctor.Univariate.M
- Cited by
- 9 results in Mathlib
- Foundations
- Depth 8 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- PFunctorstatement · cited by 75
- PFunctor.Approx.CofixAstatement · cited by 29
Cited by14
Results whose statement or proof uses this declaration.
- PFunctor.Approx.AllAgreeproof · cited by 10
- PFunctor.Approx.Agree.casesOnstatement and proof · cited by 3
- PFunctor.M.extproof · cited by 1
- PFunctor.Approx.Agree.belowstatement · cited by 1
- PFunctor.Approx.P_corecstatement and proof · cited by 1
- PFunctor.Approx.truncate_eq_of_agreestatement and proof · cited by 1
- PFunctor.M.agree_iff_agree'statement and proof · cited by 1
- PFunctor.M.default_consistentstatement · cited by 0
- PFunctor.M.Approx.P_mkproof · cited by 0
- PFunctor.Approx.Agree.below.casesOnstatement and proof · cited by 0
- PFunctor.Approx.Agree.brecOnstatement and proof · cited by 0
- PFunctor.Approx.Agree.recOnstatement and proof · cited by 0