mathlib documentation

data.finset.option

Finite sets in `option α` #

In this file we define

option.to_finset: construct an empty or singleton finset α from an option α;
finset.insert_none: given s : finset α, lift it to a finset on option α using option.some and then insert option.none;
finset.erase_none: 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.to_finset {α : Type u_1} (o : option α) :

Construct an empty or singleton finset from an option

Equations

o.to_finset = o.elim ∅ singleton

@[simp]

theorem option.to_finset_none {α : Type u_1} :

none.to_finset = ∅

@[simp]

theorem option.to_finset_some {α : Type u_1} {a : α} :

(some a).to_finset = {a}

@[simp]

theorem option.mem_to_finset {α : Type u_1} {a : α} {o : option α} :

a ∈ o.to_finset ↔ a ∈ o

theorem option.card_to_finset {α : Type u_1} (o : option α) :

o.to_finset.card = o.elim 0 1

def finset.insert_none {α : 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.insert_none = order_embedding.of_map_le_iff (λ (s : finset α), finset.cons none (finset.map function.embedding.some s) _) finset.insert_none._proof_2

@[simp]

theorem finset.mem_insert_none {α : Type u_1} {s : finset α} {o : option α} :

o ∈ ⇑finset.insert_none s ↔ ∀ (a : α), a ∈ o → a ∈ s

theorem finset.some_mem_insert_none {α : Type u_1} {s : finset α} {a : α} :

some a ∈ ⇑finset.insert_none s ↔ a ∈ s

@[simp]

theorem finset.card_insert_none {α : Type u_1} (s : finset α) :

(⇑finset.insert_none s).card = s.card + 1

def finset.erase_none {α : Type u_1} :

finset (option α) →o finset α

Given s : finset (option α), s.erase_none : finset α is the set of x : α such that some x ∈ s.

Equations

finset.erase_none = (finset.map_embedding (equiv.option_is_some_equiv α).to_embedding).to_order_hom.comp {to_fun := finset.subtype (λ (x : option α), ↥(x.is_some)) (λ (a : option α), bool.decidable_eq a.is_some tt), monotone' := _}

@[simp]

theorem finset.mem_erase_none {α : Type u_1} {s : finset (option α)} {x : α} :

x ∈ ⇑finset.erase_none s ↔ some x ∈ s

theorem finset.erase_none_eq_bUnion {α : Type u_1} [decidable_eq α] (s : finset (option α)) :

⇑finset.erase_none s = s.bUnion option.to_finset

@[simp]

theorem finset.erase_none_map_some {α : Type u_1} (s : finset α) :

⇑finset.erase_none (finset.map function.embedding.some s) = s

@[simp]

theorem finset.erase_none_image_some {α : Type u_1} [decidable_eq (option α)] (s : finset α) :

⇑finset.erase_none (finset.image some s) = s

@[simp]

theorem finset.coe_erase_none {α : Type u_1} (s : finset (option α)) :

↑(⇑finset.erase_none s) = some ⁻¹' ↑s

@[simp]

theorem finset.erase_none_union {α : Type u_1} [decidable_eq (option α)] [decidable_eq α] (s t : finset (option α)) :

⇑finset.erase_none (s ∪ t) = ⇑finset.erase_none s ∪ ⇑finset.erase_none t

@[simp]

theorem finset.erase_none_inter {α : Type u_1} [decidable_eq (option α)] [decidable_eq α] (s t : finset (option α)) :

⇑finset.erase_none (s ∩ t) = ⇑finset.erase_none s ∩ ⇑finset.erase_none t

@[simp]

theorem finset.erase_none_empty {α : Type u_1} :

⇑finset.erase_none ∅ = ∅

@[simp]

theorem finset.erase_none_none {α : Type u_1} :

⇑finset.erase_none {none} = ∅

@[simp]

theorem finset.image_some_erase_none {α : Type u_1} [decidable_eq (option α)] (s : finset (option α)) :

finset.image some (⇑finset.erase_none s) = s.erase none

@[simp]

theorem finset.map_some_erase_none {α : Type u_1} [decidable_eq (option α)] (s : finset (option α)) :

finset.map function.embedding.some (⇑finset.erase_none s) = s.erase none

@[simp]

theorem finset.insert_none_erase_none {α : Type u_1} [decidable_eq (option α)] (s : finset (option α)) :

⇑finset.insert_none (⇑finset.erase_none s) = insert none s

@[simp]

theorem finset.erase_none_insert_none {α : Type u_1} (s : finset α) :

⇑finset.erase_none (⇑finset.insert_none s) = s