Theorems · Definition · category theory

Profinite.NobelingProof.ProjRestrict

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

The restriction of Proj π J to a subset, mapping to its image.

Defined in

Mathlib.Topology.Category.Profinite.Nobeling.Basic

Cited by

13 results in Mathlib

Foundations

Depth 8 from the axioms · uses no axioms

Assumes

Decidable