Theorems · Definition · category theory

Profinite.NobelingProof.ProjRestricts

{I : Type u} →
  (C : Set (I → Bool)) →
    {J K : I → Prop} →
      [inst : (i : I) → Decidable (J i)] →
        [inst_1 : (i : I) → Decidable (K i)] →
          (∀ (i : I), J i → K i) → ↑(Profinite.NobelingProof.π C K) → ↑(Profinite.NobelingProof.π C J)

A variant of ProjRestrict with domain of the form π C K

Defined in

Mathlib.Topology.Category.Profinite.Nobeling.Basic

Cited by

12 results in Mathlib

Foundations

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

Assumes

DecidableDecidable