# mathlib3documentation

data.set.enumerate

# Set enumeration #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 α ) :

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
• s (n + 1) = sel s >>= λ (a : α), (s \ {a}) n
• s 0 = sel s
theorem set.enumerate_eq_none_of_sel {α : Type u_1} (sel : set α ) {s : set α} (h : sel s = option.none) {n : } :
theorem set.enumerate_eq_none {α : Type u_1} (sel : set α ) {s : set α} {n₁ n₂ : } :
s n₁ = option.none n₁ n₂ s n₂ = option.none
theorem set.enumerate_mem {α : Type u_1} (sel : set α ) (h_sel : (s : set α) (a : α), sel s = a s) {s : set α} {n : } {a : α} :
s n = a s
theorem set.enumerate_inj {α : Type u_1} (sel : set α ) {n₁ n₂ : } {a : α} {s : set α} (h_sel : (s : set α) (a : α), sel s = a s) (h₁ : s n₁ = ) (h₂ : s n₂ = ) :
n₁ = n₂