Theorems · Theorem · category theory

Profinite.NobelingProof.GoodProducts.span_iff_products

∀ {I : Type u} (C : Set (I → Bool)) [inst : LinearOrder I] [WellFoundedLT I],
  ⊤ ≤ Submodule.span ℤ (Set.range (Profinite.NobelingProof.GoodProducts.eval C)) ↔
    ⊤ ≤ Submodule.span ℤ (Set.range (Profinite.NobelingProof.Products.eval C))

The good products span LocallyConstant C ℤ if and only all the products do.

Defined in

Mathlib.Topology.Category.Profinite.Nobeling.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

LinearOrderWellFoundedLT