mathlib documentation

data.set.enumerate

def set.enumerate {α : Type u_1} :
(set αoption α)set αoption α

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

theorem set.enumerate_eq_none {α : Type u_1} (sel : set αoption α) {s : set α} {n₁ n₂ : } :
set.enumerate sel s n₁ = nonen₁ 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 aa s) {s : set α} {n : } {a : α} :
set.enumerate sel s n = some aa s

theorem set.enumerate_inj {α : Type u_1} (sel : set αoption α) {n₁ n₂ : } {a : α} {s : set α} :
(∀ (s : set α) (a : α), sel s = some aa s)set.enumerate sel s n₁ = some aset.enumerate sel s n₂ = some an₁ = n₂