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.
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_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 α}
(h_sel : ∀ (s : set α) (a : α), sel s = option.some a → a ∈ s)
(h₁ : set.enumerate sel s n₁ = option.some a)
(h₂ : set.enumerate sel s n₂ = option.some a) :
n₁ = n₂