Theorems · Definition · category theory

CompHausLike.LocallyConstant.sigmaIncl

{P : TopCat → Prop} →
  [inst : ∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), CompHausLike.HasProp P (Subtype p)] →
    {Q : CompHausLike P} →
      {Z : Type (max u w)} →
        (r : LocallyConstant (↑Q.toTop) Z) → (a : Function.Fiber ⇑r) → CompHausLike.LocallyConstant.fiber r a ⟶ Q

The inclusion map from a component of the coproduct induced by f into S.

Defined in

Mathlib.Condensed.Discrete.LocallyConstant

Cited by

7 results in Mathlib

Foundations

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

Assumes

CompHausLike.HasProp