Theorems · Theorem · category theory

Profinite.NobelingProof.Products.evalFacProp

∀ {I : Type u} (C : Set (I → Bool)) [inst : LinearOrder I] {l : Profinite.NobelingProof.Products I} (J : I → Prop),
  (∀ a ∈ ↑l, J a) →
    ∀ [inst_1 : (j : I) → Decidable (J j)],
      ⇑(Profinite.NobelingProof.Products.eval (Profinite.NobelingProof.π C J) l) ∘
          Profinite.NobelingProof.ProjRestrict C J =
        ⇑(Profinite.NobelingProof.Products.eval C l)

Defined in

Mathlib.Topology.Category.Profinite.Nobeling.Basic

Cited by

3 results in Mathlib

Foundations

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

Assumes

LinearOrderDecidable