mathlib documentation

data.finset.option

Finite sets in option α #

In this file we define

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 : α} :
(some a).to_finset = {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 α} :
o finset.insert_none s ∀ (a : α), a oa s
theorem finset.some_mem_insert_none {α : Type u_1} {s : finset α} {a : α} :
@[simp]
theorem finset.card_insert_none {α : Type u_1} (s : finset α) :
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 : α} :
@[simp]
@[simp]
theorem finset.coe_erase_none {α : Type u_1} (s : finset (option α)) :
@[simp]
@[simp]
theorem finset.erase_none_none {α : Type u_1} :
@[simp]