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

• o.toFinset = o.elim ∅ singleton

@[simp]

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

@[simp]

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

@[simp]

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

theorem Option.card_toFinset {α : Type u_1} (o : Option α) : o.toFinset.card = o.elim 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 ∈ insertNone s ↔ ∀ a ∈ o, a ∈ s

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

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

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

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

@[simp]

theorem Finset.card_insertNone {α : Type u_1} (s : 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

• Finset.eraseNone = (Finset.mapEmbedding (Equiv.optionIsSomeEquiv α).toEmbedding).toOrderHom.comp { toFun := Finset.subtype fun (x : Option α) => x.isSome = true, monotone' := ⋯ }

@[simp]

theorem Finset.mem_eraseNone {α : Type u_1} {s : Finset (Option α)} {x : α} : x ∈ eraseNone s ↔ some x ∈ s

theorem Finset.forall_mem_eraseNone {α : Type u_1} {s : Finset (Option α)} {p : Option α → Prop} : (∀ a ∈ eraseNone s, p (some a)) ↔ ∀ (a : α), some a ∈ s → p (some a)

theorem Finset.eraseNone_eq_biUnion {α : Type u_1} [DecidableEq α] (s : Finset (Option α)) : eraseNone s = s.biUnion Option.toFinset

@[simp]

theorem Finset.eraseNone_map_some {α : Type u_1} (s : Finset α) : eraseNone (map Function.Embedding.some s) = s

@[simp]

theorem Finset.eraseNone_image_some {α : Type u_1} [DecidableEq (Option α)] (s : Finset α) : eraseNone (image some s) = s

@[simp]

theorem Finset.coe_eraseNone {α : Type u_1} (s : Finset (Option α)) : ↑(eraseNone s) = some ⁻¹' ↑s

@[simp]

theorem Finset.eraseNone_union {α : Type u_1} [DecidableEq (Option α)] [DecidableEq α] (s t : Finset (Option α)) : eraseNone (s ∪ t) = eraseNone s ∪ eraseNone t

@[simp]

theorem Finset.eraseNone_inter {α : Type u_1} [DecidableEq (Option α)] [DecidableEq α] (s t : Finset (Option α)) : eraseNone (s ∩ t) = eraseNone s ∩ eraseNone t

@[simp]

theorem Finset.eraseNone_empty {α : Type u_1} : eraseNone ∅ = ∅

@[simp]

theorem Finset.eraseNone_none {α : Type u_1} : eraseNone {none} = ∅

@[simp]

theorem Finset.image_some_eraseNone {α : Type u_1} [DecidableEq (Option α)] (s : Finset (Option α)) : image some (eraseNone s) = s.erase none

@[simp]

theorem Finset.map_some_eraseNone {α : Type u_1} [DecidableEq (Option α)] (s : Finset (Option α)) : map Function.Embedding.some (eraseNone s) = s.erase none

@[simp]

theorem Finset.insertNone_eraseNone {α : Type u_1} [DecidableEq (Option α)] (s : Finset (Option α)) : insertNone (eraseNone s) = insert none s

@[simp]

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

theorem Finset.card_eraseNone_eq_card_erase {α : Type u_1} [DecidableEq (Option α)] (s : Finset (Option α)) : (eraseNone s).card = (s.erase none).card

theorem Finset.card_eraseNone_le {α : Type u_1} (s : Finset (Option α)) : (eraseNone s).card ≤ s.card

theorem Finset.card_eraseNone_of_mem {α : Type u_1} {s : Finset (Option α)} (h : none ∈ s) : (eraseNone s).card = s.card - 1

theorem Finset.card_eraseNone_of_not_mem {α : Type u_1} {s : Finset (Option α)} (h : none ∉ s) : (eraseNone s).card = s.card