mathlib3 documentation


Finite sets in option α #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

theorem option.to_finset_some {α : Type u_1} {a : α} :
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.

theorem finset.mem_insert_none {α : Type u_1} {s : finset α} {o : option α} :
o finset.insert_none s (a : α), a o a s
theorem finset.some_mem_insert_none {α : Type u_1} {s : finset α} {a : α} :
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.

theorem finset.mem_erase_none {α : Type u_1} {s : finset (option α)} {x : α} :