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 : Option α) : Finset α

Construct an empty or singleton finset from an Option

Equations

• Option.toFinset o = Option.elim o ∅ singleton

@[simp]

theorem Option.toFinset_none {α : Type u_1} : Option.toFinset none = ∅

@[simp]

theorem Option.toFinset_some {α : Type u_1} {a : α} : Option.toFinset (some a) = {a}

@[simp]

theorem Option.mem_toFinset {α : Type u_1} {a : α} {o : Option α} : a ∈ Option.toFinset o ↔ a ∈ o

theorem Option.card_toFinset {α : Type u_1} (o : Option α) : Finset.card (Option.toFinset o) = Option.elim o 0 1

def Finset.insertNone {α : Type u_1} : Finset α ↪o Finset (Option α)

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 s ↔ ∀ (a : α), a ∈ o → a ∈ s

theorem Finset.some_mem_insertNone {α : Type u_1} {s : Finset α} {a : α} : some a ∈ ↑Finset.insertNone s ↔ a ∈ s

@[simp]

theorem Finset.card_insertNone {α : Type u_1} (s : Finset α) : Finset.card (↑Finset.insertNone s) = Finset.card s + 1

def Finset.eraseNone {α : Type u_1} : Finset (Option α) →o Finset α

Given s : Finset (Option α), eraseNone s : Finset α is the set of x : α such that some x ∈ 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_biUnion {α : Type u_1} [DecidableEq α] (s : Finset (Option α)) : ↑Finset.eraseNone s = Finset.biUnion 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} [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} [DecidableEq (Option α)] [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} [DecidableEq (Option α)] [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} [DecidableEq (Option α)] (s : Finset (Option α)) : Finset.image some (↑Finset.eraseNone s) = Finset.erase s none

@[simp]

theorem Finset.map_some_eraseNone {α : Type u_1} [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} [DecidableEq (Option α)] (s : Finset (Option α)) : ↑Finset.insertNone (↑Finset.eraseNone s) = insert none s

@[simp]

theorem Finset.eraseNone_insertNone {α : Type u_1} (s : Finset α) : ↑Finset.eraseNone (↑Finset.insertNone s) = s