Theorems · Definition · category theory

Profinite.NobelingProof.GoodProducts.sum_to

{I : Type u} →
  (C : Set (I → Bool)) →
    [inst : LinearOrder I] →
      [inst_1 : WellFoundedLT I] →
        {o : Ordinal.{u}} →
          (ho : o < Ordinal.type fun x1 x2 => x1 < x2) →
            ↑(Profinite.NobelingProof.GoodProducts
                    (Profinite.NobelingProof.π C fun x => Profinite.NobelingProof.ord I x < o)) ⊕
                ↑(Profinite.NobelingProof.GoodProducts.MaxProducts C ho) →
              Profinite.NobelingProof.Products I

The inclusion map from the sum of GoodProducts (π C (ord I · < o)) and (MaxProducts C ho) to Products I.

Defined in

Mathlib.Topology.Category.Profinite.Nobeling.Successor

Cited by

2 results in Mathlib

Foundations

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

Assumes

LinearOrderWellFoundedLT