Theorems · Definition · category theory

CondensedMod.IsSolid.casesOn

{R : Type (u + 1)} →
  [inst : Ring R] →
    {A : CondensedMod R} →
      {motive : CondensedMod.IsSolid R A → Sort u_1} →
        (t : CondensedMod.IsSolid R A) →
          ((isIso_solidification_map :
                ∀ (X : Profinite),
                  CategoryTheory.IsIso
                    ((CategoryTheory.yoneda.obj A).map ((Condensed.profiniteSolidification R).app X).op)) →
              motive ⋯) →
            motive t

Defined in

Mathlib.Condensed.Solid

Cited by

0 results in Mathlib

Foundations

Depth 185 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Ring