# Finite sets in Option α#

In this file we define

• Option.toFinset: construct an empty or singleton Finset α from an Option α;
• Finset.insertNone: given s : Finset α, lift it to a finset on Option α using Option.some and then insert Option.none;
• Finset.eraseNone: 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.toFinset {α : Type u_1} (o : ) :

Construct an empty or singleton finset from an Option

Equations
• o.toFinset = o.elim singleton
Instances For
@[simp]
theorem Option.toFinset_none {α : Type u_1} :
none.toFinset =
@[simp]
theorem Option.toFinset_some {α : Type u_1} {a : α} :
(some a).toFinset = {a}
@[simp]
theorem Option.mem_toFinset {α : Type u_1} {a : α} {o : } :
a o.toFinset a o
theorem Option.card_toFinset {α : Type u_1} (o : ) :
o.toFinset.card = o.elim 0 1
def Finset.insertNone {α : Type u_1} :

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

Equations
Instances For
@[simp]
theorem Finset.mem_insertNone {α : Type u_1} {s : } {o : } :
o Finset.insertNone s ao, a s
theorem Finset.forall_mem_insertNone {α : Type u_1} {s : } {p : Prop} :
(aFinset.insertNone s, p a) p none as, p (some a)
theorem Finset.some_mem_insertNone {α : Type u_1} {s : } {a : α} :
some a Finset.insertNone s a s
theorem Finset.none_mem_insertNone {α : Type u_1} {s : } :
none Finset.insertNone s
theorem Finset.insertNone_nonempty {α : Type u_1} {s : } :
(Finset.insertNone s).Nonempty
@[simp]
theorem Finset.card_insertNone {α : Type u_1} (s : ) :
(Finset.insertNone s).card = s.card + 1
def Finset.eraseNone {α : Type u_1} :

Given s : Finset (Option α), eraseNone s : Finset α is the set of x : α such that some x ∈ s.

Equations
Instances For
@[simp]
theorem Finset.mem_eraseNone {α : Type u_1} {s : Finset ()} {x : α} :
x Finset.eraseNone s some x s
theorem Finset.forall_mem_eraseNone {α : Type u_1} {s : Finset ()} {p : Prop} :
(aFinset.eraseNone s, p (some a)) ∀ (a : α), some a sp (some a)
theorem Finset.eraseNone_eq_biUnion {α : Type u_1} [] (s : Finset ()) :
Finset.eraseNone s = s.biUnion Option.toFinset
@[simp]
theorem Finset.eraseNone_map_some {α : Type u_1} (s : ) :
Finset.eraseNone (Finset.map Function.Embedding.some s) = s
@[simp]
theorem Finset.eraseNone_image_some {α : Type u_1} [] (s : ) :
Finset.eraseNone (Finset.image some s) = s
@[simp]
theorem Finset.coe_eraseNone {α : Type u_1} (s : Finset ()) :
(Finset.eraseNone s) = some ⁻¹' s
@[simp]
theorem Finset.eraseNone_union {α : Type u_1} [] [] (s : Finset ()) (t : Finset ()) :
Finset.eraseNone (s t) = Finset.eraseNone s Finset.eraseNone t
@[simp]
theorem Finset.eraseNone_inter {α : Type u_1} [] [] (s : Finset ()) (t : Finset ()) :
Finset.eraseNone (s t) = Finset.eraseNone s Finset.eraseNone t
@[simp]
theorem Finset.eraseNone_empty {α : Type u_1} :
Finset.eraseNone =
@[simp]
theorem Finset.eraseNone_none {α : Type u_1} :
Finset.eraseNone {none} =
@[simp]
theorem Finset.image_some_eraseNone {α : Type u_1} [] (s : Finset ()) :
Finset.image some (Finset.eraseNone s) = s.erase none
@[simp]
theorem Finset.map_some_eraseNone {α : Type u_1} [] (s : Finset ()) :
Finset.map Function.Embedding.some (Finset.eraseNone s) = s.erase none
@[simp]
theorem Finset.insertNone_eraseNone {α : Type u_1} [] (s : Finset ()) :
Finset.insertNone (Finset.eraseNone s) = insert none s
@[simp]
theorem Finset.eraseNone_insertNone {α : Type u_1} (s : ) :
Finset.eraseNone (Finset.insertNone s) = s