Theorems · Definition · category theory

Profinite.NobelingProof.factors

{I : Type u} →
  (C : Set (I → Bool)) →
    [inst : LinearOrder I] →
      (s : Finset I) →
        ↑(Profinite.NobelingProof.π C fun x => x ∈ s) →
          List (LocallyConstant ↑(Profinite.NobelingProof.π C fun x => x ∈ s) ℤ)

A certain explicit list of locally constant maps. The theorem factors_prod_eq_basis shows that the product of the elements in this list is the delta function spanFinBasis C s x.

Defined in

Mathlib.Topology.Category.Profinite.Nobeling.Span

Cited by

5 results in Mathlib

Foundations

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

Assumes

LinearOrder