Theorems · Definition · category theory

Profinite.NobelingProof.C0

{I : Type u} →
  Set (I → Bool) →
    [inst : LinearOrder I] →
      [inst_1 : WellFoundedLT I] → {o : Ordinal.{u}} → (o < Ordinal.type fun x1 x2 => x1 < x2) → Set (I → Bool)

The subset of C consisting of those elements whose o-th entry is false.

Defined in

Mathlib.Topology.Category.Profinite.Nobeling.Successor

Cited by

6 results in Mathlib

Foundations

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

Assumes

LinearOrderWellFoundedLT