mathlib docs: data.set.enumerate

source

def set.enumerate {α : Type u_1} (sel : set α → option α) (a : set α) (a_1 : ℕ) :

option α

Equations

set.enumerate sel s (n + 1) = sel s >>= λ (a : α), set.enumerate sel (s \ {a}) n
set.enumerate sel s 0 = sel s

source

theorem set.enumerate_eq_none_of_sel {α : Type u_1} (sel : set α → option α) {s : set α} (h : sel s = none) {n : ℕ} :

set.enumerate sel s n = none

source

theorem set.enumerate_eq_none {α : Type u_1} (sel : set α → option α) {s : set α} {n₁ n₂ : ℕ} (a : set.enumerate sel s n₁ = none) (a_1 : n₁ ≤ n₂) :

set.enumerate sel s n₂ = none

source

theorem set.enumerate_mem {α : Type u_1} (sel : set α → option α) (h_sel : ∀ (s : set α) (a : α), sel s = some a → a ∈ s) {s : set α} {n : ℕ} {a : α} (a_1 : set.enumerate sel s n = some a) :

a ∈ s

source

theorem set.enumerate_inj {α : Type u_1} (sel : set α → option α) {n₁ n₂ : ℕ} {a : α} {s : set α} (h_sel : ∀ (s : set α) (a : α), sel s = some a → a ∈ s) (h₁ : set.enumerate sel s n₁ = some a) (h₂ : set.enumerate sel s n₂ = some a) :

n₁ = n₂