Theorems · Definition · combinatorics

AbstractSimplicialComplex.casesOn

{ι : Type u_1} →
  {motive : AbstractSimplicialComplex ι → Sort u} →
    (t : AbstractSimplicialComplex ι) →
      ((toPreAbstractSimplicialComplex : PreAbstractSimplicialComplex ι) →
          (singleton_mem : ∀ (v : ι), {v} ∈ toPreAbstractSimplicialComplex.faces) →
            motive
              { toPreAbstractSimplicialComplex := toPreAbstractSimplicialComplex, singleton_mem := singleton_mem }) →
        motive t

Defined in: Mathlib.AlgebraicTopology.SimplicialComplex.Basic
Cited by: 0 results in Mathlib
Foundations: Depth 27 from the axioms · uses propext, Quot.sound

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites5

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

Setstatement · cited by 53,352
Finsetstatement · cited by 13,712
PreAbstractSimplicialComplex.facesstatement and proof · cited by 36
PreAbstractSimplicialComplexstatement and proof · cited by 16
AbstractSimplicialComplexstatement and proof · cited by 10

Cited by2

Results whose statement or proof uses this declaration.

AbstractSimplicialComplex.noConfusionproof · cited by 0
AbstractSimplicialComplex.noConfusionTypeproof · cited by 0