Set enumeration

This file allows enumeration of sets given a choice function. The definition does not assume sel actually is a choice function, i.e. sel s ∈ s and sel s = none ↔ s = ∅. These assumptions are added to the lemmas needing them.

def Set.enumerate {α : Type u_1} (sel : Set α → Option α) : Set α → ℕ → Option α

Given a choice function sel, enumerates the elements of a set in the order a 0 = sel s, a 1 = sel (s \ {a 0}), a 2 = sel (s \ {a 0, a 1}), ... and stops when sel (s \ {a 0, ..., a n}) = none. Note that we don't require sel to be a choice function.

Equations

• Set.enumerate sel x 0 = sel x
• Set.enumerate sel x (Nat.succ n) = do let a ← sel x Set.enumerate sel (x \ {a}) n

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

theorem Set.enumerate_eq_none {α : Type u_1} (sel : Set α → Option α) {s : Set α} {n₁ : ℕ} {n₂ : ℕ} : Set.enumerate sel s n₁ = none → n₁ ≤ n₂ → Set.enumerate sel s n₂ = none

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 : α} : Set.enumerate sel s n = some a → a ∈ s

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₂