Theorems · Definition · category theory

Profinite.NobelingProof.GoodProducts.smaller

{I : Type u} →
  (C : Set (I → Bool)) → [inst : LinearOrder I] → [WellFoundedLT I] → Ordinal.{u} → Set (LocallyConstant ↑C ℤ)

The image of the GoodProducts for π C (ord I · < o) in LocallyConstant C ℤ. The name smaller refers to the setting in which we will use this, when we are mapping in GoodProducts from a smaller set, i.e. when o is a smaller ordinal than the one C is "contained" in.

Defined in

Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit

Cited by

8 results in Mathlib

Foundations

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

Assumes

LinearOrderWellFoundedLT