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

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) ⋯) ⋯

source

@[simp]

theorem Finset.mem_insertNone {α : Type u_1} {s : Finset α} {o : Option α} :

o ∈ Finset.insertNone s ↔ ∀ a ∈ o, a ∈ s

source

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)

source

theorem Finset.some_mem_insertNone {α : Type u_1} {s : Finset α} {a : α} :

some a ∈ Finset.insertNone s ↔ a ∈ s

source

theorem Finset.none_mem_insertNone {α : Type u_1} {s : Finset α} :

none ∈ Finset.insertNone s

source

theorem Finset.insertNone_nonempty {α : Type u_1} {s : Finset α} :

(Finset.insertNone s).Nonempty

source

@[simp]

theorem Finset.card_insertNone {α : Type u_1} (s : Finset α) :

(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' := ⋯ }