Theorems · Definition · category theory

CompHausLike.sigmaComparison

{P : TopCat → Prop} →
  [inst : CompHausLike.HasExplicitFiniteCoproducts P] →
    (X : CategoryTheory.Functor (CompHausLike P)ᵒᵖ (Type (max u w))) →
      {α : Type u} →
        [inst_1 : Finite α] →
          (σ : α → Type u) →
            [inst_2 : (a : α) → TopologicalSpace (σ a)] →
              [inst_3 : ∀ (a : α), CompactSpace (σ a)] →
                [inst_4 : ∀ (a : α), T2Space (σ a)] →
                  [inst_5 : ∀ (a : α), CompHausLike.HasProp P (σ a)] →
                    X.obj (Opposite.op (CompHausLike.of P ((a : α) × σ a))) ⟶
                      (a : α) → X.obj (Opposite.op (CompHausLike.of P (σ a)))

The comparison map from the value of a condensed set on a finite coproduct to the product of the values on the components.

Defined in

Mathlib.Topology.Category.CompHausLike.SigmaComparison

Cited by

5 results in Mathlib

Foundations

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

Assumes

CompHausLike.HasExplicitFiniteCoproductsFiniteTopologicalSpaceCompactSpaceT2SpaceCompHausLike.HasProp