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 α) : (Option.toFinset o).card = 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

• Finset.insertNone = OrderEmbedding.ofMapLEIff (fun (s : Finset α) => Finset.cons none (Finset.map Function.Embedding.some s) ⋯) ⋯

@[simp]

theorem Finset.mem_insertNone {α : Type u_1} {s : Finset α} {o : Option α} : o ∈ Finset.insertNone s ↔ ∀ a ∈ o, a ∈ s

theorem Finset.forall_mem_insertNone {α : Type u_1} {s : Finset α} {p : Option α → Prop} : (∀ a ∈ Finset.insertNone s, p a) ↔ p none ∧ ∀ a ∈ s, p (some a)

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

theorem Finset.none_mem_insertNone {α : Type u_1} {s : Finset α} : none ∈ Finset.insertNone s

theorem Finset.insertNone_nonempty {α : Type u_1} {s : Finset α} : (Finset.insertNone s).Nonempty

@[simp]

theorem Finset.card_insertNone {α : Type u_1} (s : Finset α) : (Finset.insertNone s).card = s.card + 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.forall_mem_eraseNone {α : Type u_1} {s : Finset (Option α)} {p : Option α → Prop} : (∀ a ∈ Finset.eraseNone s, p (some a)) ↔ ∀ (a : α), some a ∈ s → p (some a)

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