Theorems · Theorem · logic and foundations

Set.enumerateCountable_mem

∀ {α : Type u} {s : Set α} (h : s.Countable) {default : α},
  default ∈ s → ∀ (n : ℕ), Set.enumerateCountable h default n ∈ s

Defined in

Mathlib.Data.Set.Countable

Cited by

2 results in Mathlib

Foundations

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