Theorems · Theorem · category theory

Profinite.NobelingProof.Products.evalFacProps

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

Defined in

Mathlib.Topology.Category.Profinite.Nobeling.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

LinearOrderDecidableDecidable