Theorems · Theorem · logic and foundations

Set.countable_pi

∀ {α : Type u} {π : α → Type u_1} [Finite α] {s : (a : α) → Set (π a)},
  (∀ (a : α), (s a).Countable) → {f | ∀ (a : α), f a ∈ s a}.Countable

Defined in

Mathlib.Data.Set.Countable

Cited by

0 results in Mathlib

Foundations

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

Assumes

Finite