Theorems · Theorem · category theory

Profinite.NobelingProof.projRestricts_comp_projRestrict

∀ {I : Type u} (C : Set (I → Bool)) {J K : I → Prop} [inst : (i : I) → Decidable (J i)]
  [inst_1 : (i : I) → Decidable (K i)] (h : ∀ (i : I), J i → K i),
  Profinite.NobelingProof.ProjRestricts C h ∘ Profinite.NobelingProof.ProjRestrict C K =
    Profinite.NobelingProof.ProjRestrict C J

Defined in

Mathlib.Topology.Category.Profinite.Nobeling.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

DecidableDecidable