Documentation

Mathlib.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.toFinset {α : Type u_1} (o : Option α) :

Construct an empty or singleton finset from an Option

Equations
@[simp]
theorem Option.toFinset_none {α : Type u_1} :
@[simp]
theorem Option.toFinset_some {α : Type u_1} {a : α} :
@[simp]
theorem Option.mem_toFinset {α : Type u_1} {a : α} {o : Option α} :
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
  • One or more equations did not get rendered due to their size.
@[simp]
theorem Finset.mem_insertNone {α : Type u_1} {s : Finset α} {o : Option α} :
o Finset.insertNone.toEmbedding s ∀ (a : α), a oa s
theorem Finset.some_mem_insertNone {α : Type u_1} {s : Finset α} {a : α} :
some a Finset.insertNone.toEmbedding s a s
@[simp]
theorem Finset.card_insertNone {α : Type u_1} (s : Finset α) :
Finset.card (Finset.insertNone.toEmbedding s) = Finset.card s + 1
def Finset.eraseNone {α : Type u_1} :

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

Equations
  • One or more equations did not get rendered due to their size.
@[simp]
theorem Finset.mem_eraseNone {α : Type u_1} {s : Finset (Option α)} {x : α} :
x Finset.eraseNone s some x s
theorem Finset.eraseNone_eq_bunionᵢ {α : Type u_1} [inst : DecidableEq α] (s : Finset (Option α)) :
Finset.eraseNone s = Finset.bunionᵢ s Option.toFinset
@[simp]
theorem Finset.eraseNone_map_some {α : Type u_1} (s : Finset α) :
Finset.eraseNone (Finset.map Function.Embedding.some s) = s
@[simp]
theorem Finset.eraseNone_image_some {α : Type u_1} [inst : DecidableEq (Option α)] (s : Finset α) :
Finset.eraseNone (Finset.image some s) = s
@[simp]
theorem Finset.coe_eraseNone {α : Type u_1} (s : Finset (Option α)) :
↑(Finset.eraseNone s) = some ⁻¹' s
@[simp]
theorem Finset.eraseNone_union {α : Type u_1} [inst : DecidableEq (Option α)] [inst : DecidableEq α] (s : Finset (Option α)) (t : Finset (Option α)) :
Finset.eraseNone (s t) = Finset.eraseNone s Finset.eraseNone t
@[simp]
theorem Finset.eraseNone_inter {α : Type u_1} [inst : DecidableEq (Option α)] [inst : DecidableEq α] (s : Finset (Option α)) (t : Finset (Option α)) :
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} [inst : DecidableEq (Option α)] (s : Finset (Option α)) :
Finset.image some (Finset.eraseNone s) = Finset.erase s none
@[simp]
theorem Finset.map_some_eraseNone {α : Type u_1} [inst : DecidableEq (Option α)] (s : Finset (Option α)) :
Finset.map Function.Embedding.some (Finset.eraseNone s) = Finset.erase s none
@[simp]
theorem Finset.insertNone_eraseNone {α : Type u_1} [inst : DecidableEq (Option α)] (s : Finset (Option α)) :
Finset.insertNone.toEmbedding (Finset.eraseNone s) = insert none s
@[simp]
theorem Finset.eraseNone_insertNone {α : Type u_1} (s : Finset α) :
Finset.eraseNone (Finset.insertNone.toEmbedding s) = s