Theorems · Theorem · category theory

Profinite.NobelingProof.proj_eq_of_subset

∀ {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.π (Profinite.NobelingProof.π C K) J = Profinite.NobelingProof.π C J

Defined in

Mathlib.Topology.Category.Profinite.Nobeling.Basic

Cited by

3 results in Mathlib

Foundations

Depth 12 from the axioms · uses propext, Quot.sound

Assumes

DecidableDecidable