Theorems · Theorem · category theory

Profinite.NobelingProof.surjective_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)] (h : ∀ (i : I), J i → K i),
  Function.Surjective (Profinite.NobelingProof.ProjRestricts C h)

Defined in

Mathlib.Topology.Category.Profinite.Nobeling.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

DecidableDecidable