Theorems · Theorem · category theory

Profinite.NobelingProof.fin_comap_jointlySurjective

∀ {I : Type u} (C : Set (I → Bool)) [inst : LinearOrder I],
  IsClosed C →
    ∀ (f : LocallyConstant ↑C ℤ),
      ∃ s g,
        f =
          LocallyConstant.comap
            { toFun := Profinite.NobelingProof.ProjRestrict C fun x => x ∈ s, continuous_toFun := ⋯ } g

Defined in

Mathlib.Topology.Category.Profinite.Nobeling.Span

Cited by

1 results in Mathlib

Foundations

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

Assumes

LinearOrder