Theorems · Definition · category theory

Profinite.NobelingProof.GoodProducts.MaxProducts

{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 (Profinite.NobelingProof.Products I)

The GoodProducts in C that contain o (they necessarily start with o, see GoodProducts.head!_eq_o_of_maxProducts)

Defined in

Mathlib.Topology.Category.Profinite.Nobeling.Successor

Cited by

17 results in Mathlib

Foundations

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

Assumes

LinearOrderWellFoundedLT