Theorems · Theorem · category theory

Profinite.NobelingProof.Products.prop_of_isGood

∀ {I : Type u} (C : Set (I → Bool)) [inst : LinearOrder I] {l : Profinite.NobelingProof.Products I} (J : I → Prop)
  [inst_1 : (j : I) → Decidable (J j)],
  Profinite.NobelingProof.Products.isGood (Profinite.NobelingProof.π C J) l → ∀ a ∈ ↑l, J a

Defined in

Mathlib.Topology.Category.Profinite.Nobeling.Basic

Cited by

10 results in Mathlib

Foundations

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

Assumes

LinearOrderDecidable