Equations
- set.enumerate sel s (n + 1) = sel s >>= λ (a : α), set.enumerate sel (s \ {a}) n
- set.enumerate sel s 0 = sel s
theorem
set.enumerate_eq_none_of_sel
{α : Type u_1}
(sel : set α → option α)
{s : set α}
(h : sel s = option.none)
{n : ℕ} :
set.enumerate sel s n = option.none
theorem
set.enumerate_eq_none
{α : Type u_1}
(sel : set α → option α)
{s : set α}
{n₁ n₂ : ℕ} :
set.enumerate sel s n₁ = option.none → n₁ ≤ n₂ → set.enumerate sel s n₂ = option.none
theorem
set.enumerate_mem
{α : Type u_1}
(sel : set α → option α)
(h_sel : ∀ (s : set α) (a : α), sel s = option.some a → a ∈ s)
{s : set α}
{n : ℕ}
{a : α} :
set.enumerate sel s n = option.some a → a ∈ s
theorem
set.enumerate_inj
{α : Type u_1}
(sel : set α → option α)
{n₁ n₂ : ℕ}
{a : α}
{s : set α} :
(∀ (s : set α) (a : α), sel s = option.some a → a ∈ s) → set.enumerate sel s n₁ = option.some a → set.enumerate sel s n₂ = option.some a → n₁ = n₂