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.
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 s (n + 1) = sel s >>= λ (a : α), set.enumerate sel (s \ {a}) n
- set.enumerate sel s 0 = sel s
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