Mathlib Map

Theorems · Definition · general algebraic systems

DFinsupp.casesOn

{ι : Type u} →
  {β : ι → Type v} →
    [inst : (i : ι) → Zero (β i)] →
      {motive : DFinsupp β → Sort u_1} →
        (t : DFinsupp β) →
          ((toFun : (i : ι) → β i) →
              (support' : Trunc { s // ∀ (i : ι), i ∈ s ∨ toFun i = 0 }) →
                motive { toFun := toFun, support' := support' }) →
            motive t
Defined in
Mathlib.Data.DFinsupp.Defs
Cited by
6 results in Mathlib
Foundations
Depth 17 from the axioms · uses propext
Assumes
Zero
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

DFinsupp.mem_support_toFun · cited by 6DFinsupp.mem_support_toFunDFinsupp.induction · cited by 5DFinsupp.inductionDFinsupp.mapRange_surjective · cited by 2DFinsupp.mapRange_surject…DFinsupp.sumZeroHom_piSingle · cited by 1DFinsupp.sumZeroHom_piSin…DFinsupp.sumZeroHom_apply · cited by 1DFinsupp.sumZeroHom_applyDFinsupp.noConfusion · cited by 0DFinsupp.noConfusionDFinsupp.noConfusionType · cited by 0DFinsupp.noConfusionTypeDFinsupp.sumAddHom_comm · cited by 0DFinsupp.sumAddHom_commMultiset · cited by 2627MultisetDFinsupp · cited by 694DFinsuppTrunc · cited by 39TruncDFinsupp.casesOnCITED BYCITES

Cites3

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • Multisetstatement and proof · cited by 2,627
  • DFinsuppstatement and proof · cited by 694
  • Truncstatement and proof · cited by 39

Cited by8

Results whose statement or proof uses this declaration.