# 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

source
def Option.toFinset {α : Type u_1} (o : Option α) :
Finset α

Construct an empty or singleton finset from an `Option`

Equations

- o.toFinset = o.elim ∅ singleton

Instances For

source
@[simp]
theorem Option.toFinset_none {α : Type u_1} :
none.toFinset = ∅
source
@[simp]
theorem Option.toFinset_some {α : Type u_1} {a : α} :
(some a).toFinset = {a}
source
@[simp]
theorem Option.mem_toFinset {α : Type u_1} {a : α} {o : Option α} :
a ∈ o.toFinset ↔ a ∈ o
source
theorem Option.card_toFinset {α : Type u_1} (o : Option α) :
o.toFinset.card = o.elim 0 1
source
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) ⋯) ⋯

Instances For

source
@[simp]
theorem Finset.mem_insertNone {α : Type u_1} {s : Finset α} {o : Option α} :
o ∈ insertNone s ↔ ∀ a ∈ o, a ∈ s
source
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)
source
theorem Finset.some_mem_insertNone {α : Type u_1} {s : Finset α} {a : α} :
some a ∈ insertNone s ↔ a ∈ s
source
theorem Finset.none_mem_insertNone {α : Type u_1} {s : Finset α} :
none ∈ insertNone s
source
theorem Finset.insertNone_nonempty {α : Type u_1} {s : Finset α} :
(insertNone s).Nonempty
source
@[simp]
theorem Finset.card_insertNone {α : Type u_1} (s : Finset α) :
(insertNone s).card = s.card + 1
source
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' := ⋯ }

Instances For

source
@[simp]
theorem Finset.mem_eraseNone {α : Type u_1} {s : Finset (Option α)} {x : α} :
x ∈ eraseNone s ↔ some x ∈ s
source
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)
source
theorem Finset.eraseNone_eq_biUnion {α : Type u_1} [DecidableEq α] (s : Finset (Option α)) :
eraseNone s = s.biUnion Option.toFinset
source
@[simp]
theorem Finset.eraseNone_map_some {α : Type u_1} (s : Finset α) :
eraseNone (map Function.Embedding.some s) = s
source
@[simp]
theorem Finset.eraseNone_image_some {α : Type u_1} [DecidableEq (Option α)] (s : Finset α) :
eraseNone (image some s) = s
source
@[simp]
theorem Finset.coe_eraseNone {α : Type u_1} (s : Finset (Option α)) :
↑(eraseNone s) = some ⁻¹' ↑s
source
@[simp]
theorem Finset.eraseNone_union {α : Type u_1} [DecidableEq (Option α)] [DecidableEq α] (s t : Finset (Option α)) :
eraseNone (s ∪ t) = eraseNone s ∪ eraseNone t
source
@[simp]
theorem Finset.eraseNone_inter {α : Type u_1} [DecidableEq (Option α)] [DecidableEq α] (s t : Finset (Option α)) :
eraseNone (s ∩ t) = eraseNone s ∩ eraseNone t
source
@[simp]
theorem Finset.eraseNone_empty {α : Type u_1} :
eraseNone ∅ = ∅
source
@[simp]
theorem Finset.eraseNone_none {α : Type u_1} :
eraseNone {none} = ∅
source
@[simp]
theorem Finset.image_some_eraseNone {α : Type u_1} [DecidableEq (Option α)] (s : Finset (Option α)) :
image some (eraseNone s) = s.erase none
source
@[simp]
theorem Finset.map_some_eraseNone {α : Type u_1} [DecidableEq (Option α)] (s : Finset (Option α)) :
map Function.Embedding.some (eraseNone s) = s.erase none
source
@[simp]
theorem Finset.insertNone_eraseNone {α : Type u_1} [DecidableEq (Option α)] (s : Finset (Option α)) :
insertNone (eraseNone s) = insert none s
source
@[simp]
theorem Finset.eraseNone_insertNone {α : Type u_1} (s : Finset α) :
eraseNone (insertNone s) = s
source
theorem Finset.card_eraseNone_eq_card_erase {α : Type u_1} [DecidableEq (Option α)] (s : Finset (Option α)) :
(eraseNone s).card = (s.erase none).card
source
theorem Finset.card_eraseNone_le {α : Type u_1} (s : Finset (Option α)) :
(eraseNone s).card ≤ s.card
source
theorem Finset.card_eraseNone_of_mem {α : Type u_1} {s : Finset (Option α)} (h : none ∈ s) :
(eraseNone s).card = s.card - 1
source
theorem Finset.card_eraseNone_of_not_mem {α : Type u_1} {s : Finset (Option α)} (h : none ∉ s) :
(eraseNone s).card = s.card