# mathlibdocumentation

data.finset.option

# Finite sets in option α#

In this file we define

• option.to_finset: construct an empty or singleton finset α from an option α;
• finset.insert_none: given s : finset α, lift it to a finset on option α using option.some and then insert option.none;
• finset.erase_none: given s : finset (option α), returns t : finset α such that x ∈ t ↔ some x ∈ s.

Then we prove some basic lemmas about these definitions.

## Tags #

finset, option

def option.to_finset {α : Type u_1} (o : option α) :

Construct an empty or singleton finset from an option

Equations
@[simp]
theorem option.to_finset_none {α : Type u_1} :
@[simp]
theorem option.to_finset_some {α : Type u_1} {a : α} :
@[simp]
theorem option.mem_to_finset {α : Type u_1} {a : α} {o : option α} :
theorem option.card_to_finset {α : Type u_1} (o : option α) :
def finset.insert_none {α : Type u_1} :

Given a finset on α, lift it to being a finset on option α using option.some and then insert option.none.

Equations
@[simp]
theorem finset.mem_insert_none {α : Type u_1} {s : finset α} {o : option α} :
∀ (a : α), a oa s
theorem finset.some_mem_insert_none {α : Type u_1} {s : finset α} {a : α} :
a s
@[simp]
theorem finset.card_insert_none {α : Type u_1} (s : finset α) :
= s.card + 1
def finset.erase_none {α : Type u_1} :

Given s : finset (option α), s.erase_none : finset α is the set of x : α such that some x ∈ s.

Equations
@[simp]
theorem finset.mem_erase_none {α : Type u_1} {s : finset (option α)} {x : α} :
s
theorem finset.erase_none_eq_bUnion {α : Type u_1} [decidable_eq α] (s : finset (option α)) :
@[simp]
theorem finset.erase_none_map_some {α : Type u_1} (s : finset α) :
@[simp]
theorem finset.erase_none_image_some {α : Type u_1} [decidable_eq (option α)] (s : finset α) :
@[simp]
theorem finset.coe_erase_none {α : Type u_1} (s : finset (option α)) :
@[simp]
theorem finset.erase_none_union {α : Type u_1} [decidable_eq (option α)] [decidable_eq α] (s t : finset (option α)) :
@[simp]
theorem finset.erase_none_inter {α : Type u_1} [decidable_eq (option α)] [decidable_eq α] (s t : finset (option α)) :
@[simp]
theorem finset.erase_none_empty {α : Type u_1} :
@[simp]
theorem finset.erase_none_none {α : Type u_1} :
@[simp]
theorem finset.image_some_erase_none {α : Type u_1} [decidable_eq (option α)] (s : finset (option α)) :
@[simp]
theorem finset.map_some_erase_none {α : Type u_1} [decidable_eq (option α)] (s : finset (option α)) :
@[simp]
theorem finset.insert_none_erase_none {α : Type u_1} [decidable_eq (option α)] (s : finset (option α)) :
@[simp]
theorem finset.erase_none_insert_none {α : Type u_1} (s : finset α) :