Mathlib.Data.Finset.Option

Option.toFinset definition

(o : Option α) : Finset α

Full source

/-- Construct an empty or singleton finset from an `Option` -/
def toFinset (o : Option α) : Finset α :=
  o.elim ∅ singleton

Conversion from Option to Finite Set

Informal description

Given an option type `Option α`, the function constructs either an empty finite set (when the input is `none`) or a singleton finite set containing the element (when the input is `some a`).

Option.toFinset_none theorem

: none.toFinset = (∅ : Finset α)

Full source

@[simp]
theorem toFinset_none : none.toFinset = (∅ : Finset α) :=
  rfl

Empty Set Construction from None Option

Informal description

The finite set constructed from the `none` option is equal to the empty finite set, i.e., $\text{none.toFinset} = \emptyset$.

Option.toFinset_some theorem

{a : α} : (some a).toFinset = { a }

Full source

@[simp]
theorem toFinset_some {a : α} : (some a).toFinset = {a} :=
  rfl

Singleton Construction from Some Option: $\text{some }a\text{.toFinset} = \{a\}$

Informal description

For any element $a$ of type $\alpha$, the finite set constructed from the option `some a` is equal to the singleton set $\{a\}$.

Option.mem_toFinset theorem

{a : α} {o : Option α} : a ∈ o.toFinset ↔ a ∈ o

Full source

@[simp]
theorem mem_toFinset {a : α} {o : Option α} : a ∈ o.toFinseta ∈ o.toFinset ↔ a ∈ o := by
  cases o <;> simp [eq_comm]

Membership in Option-to-Finite-Set Conversion

Informal description

For any element $a$ of type $\alpha$ and any option $o$ of type $\text{Option }\alpha$, the element $a$ belongs to the finite set constructed from $o$ (i.e., $a \in o.\text{toFinset}$) if and only if $a$ is contained in $o$ (i.e., $a \in o$).

Option.card_toFinset theorem

(o : Option α) : o.toFinset.card = o.elim 0 1

Full source

theorem card_toFinset (o : Option α) : o.toFinset.card = o.elim 0 1 := by cases o <;> rfl

Cardinality of Option to Finite Set Conversion

Informal description

For any option type `Option α`, the cardinality of the finite set obtained by converting the option `o` is equal to 0 if `o` is `none` and 1 if `o` is `some a` for some `a : α`. In other words, $|\text{toFinset}(o)| = \begin{cases} 0 & \text{if } o = \text{none} \\ 1 & \text{if } o = \text{some } a \end{cases}$.

Finset.insertNone definition

: Finset α ↪o Finset (Option α)

Full source

/-- Given a finset on `α`, lift it to being a finset on `Option α`
using `Option.some` and then insert `Option.none`. -/
def insertNone : FinsetFinset α ↪o Finset (Option α) :=
  (OrderEmbedding.ofMapLEIff fun s => cons none (s.map Embedding.some) <| by simp) fun s t => by
    rw [le_iff_subset, cons_subset_cons, map_subset_map, le_iff_subset]

Order embedding of finite sets into Option type via insertion of none

Informal description

Given a finite set $s$ of type $\alpha$, the function $\text{insertNone}$ constructs a finite set of type $\operatorname{Option} \alpha$ by embedding $s$ into $\operatorname{Option} \alpha$ via the $\operatorname{some}$ constructor and then inserting $\operatorname{none}$. This operation forms an order embedding between the finite sets of $\alpha$ and $\operatorname{Option} \alpha$, preserving the subset relation.

Finset.mem_insertNone theorem

{s : Finset α} : ∀ {o : Option α}, o ∈ insertNone s ↔ ∀ a ∈ o, a ∈ s

Full source

@[simp]
theorem mem_insertNone {s : Finset α} : ∀ {o : Option α}, o ∈ insertNone so ∈ insertNone s ↔ ∀ a ∈ o, a ∈ s
  | none => iff_of_true (Multiset.mem_cons_self _ _) fun a h => by cases h
  | some a => Multiset.mem_cons.trans <| by simp

Membership in `insertNone` Finite Set: $o \in \operatorname{insertNone}(s) \leftrightarrow (\forall a \in o, a \in s)$

Informal description

For any finite set $s$ of type $\alpha$ and any option $o$ of type $\operatorname{Option} \alpha$, the option $o$ is an element of the finite set $\operatorname{insertNone}(s)$ if and only if every element $a$ in $o$ (when $o$ is $\operatorname{some}(a)$) belongs to $s$. In other words, $o \in \operatorname{insertNone}(s) \leftrightarrow (\forall a \in o, a \in s)$.

Finset.forall_mem_insertNone theorem

{s : Finset α} {p : Option α → Prop} : (∀ a ∈ insertNone s, p a) ↔ p none ∧ ∀ a ∈ s, p a

Full source

lemma forall_mem_insertNone {s : Finset α} {p : Option α → Prop} :
    (∀ a ∈ insertNone s, p a) ↔ p none ∧ ∀ a ∈ s, p a := by simp [Option.forall]

Universal Property of Lifted Finite Sets with None

Informal description

For any finite set $s$ of type $\alpha$ and any predicate $p$ on $\operatorname{Option} \alpha$, the following equivalence holds: every element in the set $\text{insertNone}(s)$ satisfies $p$ if and only if $p$ holds for $\operatorname{none}$ and for every $a \in s$, $p(\operatorname{some}(a))$ holds.

Finset.some_mem_insertNone theorem

{s : Finset α} {a : α} : some a ∈ insertNone s ↔ a ∈ s

Full source

theorem some_mem_insertNone {s : Finset α} {a : α} : somesome a ∈ insertNone ssome a ∈ insertNone s ↔ a ∈ s := by simp

Membership of Some Element in Inserted None Finite Set

Informal description

For any finite set $s$ of type $\alpha$ and any element $a \in \alpha$, the element $\operatorname{some}(a)$ belongs to the finite set $\operatorname{insertNone}(s)$ if and only if $a$ belongs to $s$.

Finset.none_mem_insertNone theorem

{s : Finset α} : none ∈ insertNone s

Full source

lemma none_mem_insertNone {s : Finset α} : nonenone ∈ insertNone s := by simp

Membership of None in Inserted Finite Set

Informal description

For any finite set $s$ of type $\alpha$, the element $\operatorname{none}$ is a member of the finite set $\operatorname{insertNone}(s)$ of type $\operatorname{Option} \alpha$.

Finset.insertNone_nonempty theorem

{s : Finset α} : insertNone s |>.Nonempty

Full source

@[aesop safe apply (rule_sets := [finsetNonempty])]
lemma insertNone_nonempty {s : Finset α} : insertNone s |>.Nonempty := ⟨none, none_mem_insertNone⟩

Nonemptiness of Finite Set with Inserted None Element

Informal description

For any finite set $s$ of type $\alpha$, the finite set $\operatorname{insertNone}(s)$ is nonempty.

Finset.card_insertNone theorem

(s : Finset α) : s.insertNone.card = s.card + 1

Full source

@[simp]
theorem card_insertNone (s : Finset α) : s.insertNone.card = s.card + 1 := by simp [insertNone]

Cardinality of Finite Set with Inserted None Element

Informal description

For any finite set $s$ of type $\alpha$, the cardinality of the finite set obtained by applying the $\text{insertNone}$ operation to $s$ is equal to the cardinality of $s$ plus one, i.e., $|\text{insertNone}(s)| = |s| + 1$.

Finset.eraseNone definition

: Finset (Option α) →o Finset α

Full source

/-- Given `s : Finset (Option α)`, `eraseNone s : Finset α` is the set of `x : α` such that
`some x ∈ s`. -/
def eraseNone : FinsetFinset (Option α) →o Finset α :=
  (Finset.mapEmbedding (Equiv.optionIsSomeEquiv α).toEmbedding).toOrderHom.comp
    ⟨Finset.subtype _, subtype_mono⟩

Finite set of underlying values from option type

Informal description

Given a finite set `s` of elements of type `Option α`, `eraseNone s` is the finite set of elements `x : α` such that `some x ∈ s`. This is constructed by first taking the subset of `s` consisting of elements that are `some a` (i.e., non-`none`), then mapping each `some a` to its underlying value `a`. More formally, `eraseNone` is an order homomorphism from finite sets of `Option α` to finite sets of `α` that preserves the subset relation.

Finset.mem_eraseNone theorem

{s : Finset (Option α)} {x : α} : x ∈ eraseNone s ↔ some x ∈ s

Full source

@[simp]
theorem mem_eraseNone {s : Finset (Option α)} {x : α} : x ∈ eraseNone sx ∈ eraseNone s ↔ some x ∈ s := by
  simp [eraseNone]

Membership in $\text{eraseNone}(s)$ is equivalent to $\text{some } x$ being in $s$

Informal description

For any finite set $s$ of elements of type $\text{Option } \alpha$ and any element $x \in \alpha$, $x$ belongs to the finite set $\text{eraseNone}(s)$ if and only if $\text{some } x$ belongs to $s$.

Finset.forall_mem_eraseNone theorem

 {s : Finset (Option α)} {p : Option α → Prop} : (∀ a ∈ eraseNone s, p a) ↔ ∀ a : α, (a : Option α) ∈ s → p a

Full source

lemma forall_mem_eraseNone {s : Finset (Option α)} {p : Option α → Prop} :
    (∀ a ∈ eraseNone s, p a) ↔ ∀ a : α, (a : Option α) ∈ s → p a := by simp [Option.forall]

Characterization of Predicate Satisfaction on $\text{eraseNone } s$ via $\text{some } a \in s$

Informal description

For any finite set $s$ of elements of type $\text{Option } \alpha$ and any predicate $p$ on $\text{Option } \alpha$, the following are equivalent: 1. For every element $a$ in the finite set $\text{eraseNone } s$, the predicate $p(a)$ holds. 2. For every element $a$ of type $\alpha$, if $\text{some } a$ is in $s$, then $p(a)$ holds.

Finset.eraseNone_eq_biUnion theorem

[DecidableEq α] (s : Finset (Option α)) : eraseNone s = s.biUnion Option.toFinset

Full source

theorem eraseNone_eq_biUnion [DecidableEq α] (s : Finset (Option α)) :
    eraseNone s = s.biUnion Option.toFinset := by
  ext
  simp

Equality between $\text{eraseNone}$ and finite union of $\text{Option.toFinset}$ applications

Informal description

For any finite set $s$ of elements of type $\text{Option}\,\alpha$ (where $\alpha$ has decidable equality), the set obtained by removing all `none` elements from $s$ is equal to the finite union of the sets obtained by applying $\text{Option.toFinset}$ to each element of $s$. That is, $$\text{eraseNone}\,s = \bigcup_{x \in s} \text{Option.toFinset}\,x.$$

Finset.eraseNone_map_some theorem

(s : Finset α) : eraseNone (s.map Embedding.some) = s

Full source

@[simp]
theorem eraseNone_map_some (s : Finset α) : eraseNone (s.map Embedding.some) = s := by
  ext
  simp

Erasing Nones from Mapped Some Preserves Original Finite Set

Informal description

For any finite set $s$ of elements of type $\alpha$, the operation of first mapping each element $x \in s$ to $\operatorname{some}(x)$ (using the embedding $\alpha \hookrightarrow \operatorname{Option} \alpha$) and then applying the $\operatorname{eraseNone}$ function returns the original set $s$. In other words, $\operatorname{eraseNone}(\operatorname{map}(\operatorname{some}, s)) = s$.

Finset.eraseNone_image_some theorem

[DecidableEq (Option α)] (s : Finset α) : eraseNone (s.image some) = s

Full source

@[simp]
theorem eraseNone_image_some [DecidableEq (Option α)] (s : Finset α) :
    eraseNone (s.image some) = s := by simpa only [map_eq_image] using eraseNone_map_some s

Image under `some` followed by `eraseNone` preserves finite sets

Informal description

For any finite set $s$ of elements of type $\alpha$, the operation of first taking the image of $s$ under the `some` function (mapping each $x \in \alpha$ to $\operatorname{some}(x) \in \operatorname{Option} \alpha$) and then applying the `eraseNone` function returns the original set $s$. In other words, $\operatorname{eraseNone}(\operatorname{image}(\operatorname{some}, s)) = s$.

Finset.coe_eraseNone theorem

(s : Finset (Option α)) : (eraseNone s : Set α) = some ⁻¹' s

Full source

@[simp]
theorem coe_eraseNone (s : Finset (Option α)) : (eraseNone s : Set α) = somesome ⁻¹' s :=
  Set.ext fun _ => mem_eraseNone

Set Equality for $\text{eraseNone}(s)$ as Preimage of $\text{some}$

Informal description

For any finite set $s$ of elements of type $\text{Option } \alpha$, the underlying set of $\text{eraseNone}(s)$ is equal to the preimage of $s$ under the $\text{some}$ function. In other words, the set $\{x \in \alpha \mid x \in \text{eraseNone}(s)\}$ is equal to $\{x \in \alpha \mid \text{some } x \in s\}$.

Finset.eraseNone_union theorem

 [DecidableEq (Option α)] [DecidableEq α] (s t : Finset (Option α)) : eraseNone (s ∪ t) = eraseNone s ∪ eraseNone t

Full source

@[simp]
theorem eraseNone_union [DecidableEq (Option α)] [DecidableEq α] (s t : Finset (Option α)) :
    eraseNone (s ∪ t) = eraseNoneeraseNone s ∪ eraseNone t := by
  ext
  simp

$\text{eraseNone}$ Preserves Union of Finite Option Sets

Informal description

For any two finite sets $s$ and $t$ of elements of type $\text{Option } \alpha$, the operation $\text{eraseNone}$ commutes with the union operation, i.e., \[ \text{eraseNone}(s \cup t) = \text{eraseNone}(s) \cup \text{eraseNone}(t). \] Here, $\text{eraseNone}(s)$ denotes the finite set of all $x \in \alpha$ such that $\text{some } x \in s$.

Finset.eraseNone_inter theorem

 [DecidableEq (Option α)] [DecidableEq α] (s t : Finset (Option α)) : eraseNone (s ∩ t) = eraseNone s ∩ eraseNone t

Full source

@[simp]
theorem eraseNone_inter [DecidableEq (Option α)] [DecidableEq α] (s t : Finset (Option α)) :
    eraseNone (s ∩ t) = eraseNoneeraseNone s ∩ eraseNone t := by
  ext
  simp

$\text{eraseNone}$ Preserves Finite Set Intersection

Informal description

For any two finite sets $s$ and $t$ of elements of type $\text{Option } \alpha$, the operation $\text{eraseNone}$ commutes with intersection, i.e., $\text{eraseNone}(s \cap t) = \text{eraseNone}(s) \cap \text{eraseNone}(t)$.

Finset.eraseNone_empty theorem

: eraseNone (∅ : Finset (Option α)) = ∅

Full source

@[simp]
theorem eraseNone_empty : eraseNone (∅ : Finset (Option α)) = ∅ := by
  ext
  simp

`eraseNone` Preserves the Empty Set

Informal description

For the empty finite set of elements of type `Option α`, the operation `eraseNone` returns the empty finite set of elements of type `α`. That is, $\text{eraseNone}(\emptyset) = \emptyset$.

Finset.eraseNone_none theorem

: eraseNone ({ none } : Finset (Option α)) = ∅

Full source

@[simp]
theorem eraseNone_none : eraseNone ({none} : Finset (Option α)) = ∅ := by
  ext
  simp

$\text{eraseNone}$ of $\{\text{none}\}$ is empty

Informal description

For the finite set $\{\text{none}\}$ of type $\text{Option}\,\alpha$, the operation $\text{eraseNone}$ returns the empty set $\emptyset$.

Finset.image_some_eraseNone theorem

[DecidableEq (Option α)] (s : Finset (Option α)) : (eraseNone s).image some = s.erase none

Full source

@[simp]
theorem image_some_eraseNone [DecidableEq (Option α)] (s : Finset (Option α)) :
    (eraseNone s).image some = s.erase none := by ext (_ | x) <;> simp

Image of $\text{eraseNone}$ under $\text{some}$ equals $s$ without $\text{none}$

Informal description

For any finite set $s$ of elements of type $\text{Option}\,\alpha$ (with decidable equality), the image of the finite set $\text{eraseNone}\,s$ under the $\text{some}$ function is equal to the finite set obtained by removing $\text{none}$ from $s$. That is, $\text{some}[\text{eraseNone}\,s] = s \setminus \{\text{none}\}$.

Finset.map_some_eraseNone theorem

[DecidableEq (Option α)] (s : Finset (Option α)) : (eraseNone s).map Embedding.some = s.erase none

Full source

@[simp]
theorem map_some_eraseNone [DecidableEq (Option α)] (s : Finset (Option α)) :
    (eraseNone s).map Embedding.some = s.erase none := by
  rw [map_eq_image, Embedding.some_apply, image_some_eraseNone]

Image of $\operatorname{eraseNone}$ under $\operatorname{some}$ embedding equals $s$ without $\operatorname{none}$

Informal description

For any finite set $s$ of elements of type $\operatorname{Option} \alpha$ (with decidable equality), the image of the finite set $\operatorname{eraseNone} s$ under the injective embedding $\operatorname{some} : \alpha \hookrightarrow \operatorname{Option} \alpha$ is equal to the finite set obtained by removing $\operatorname{none}$ from $s$. That is, $$ \operatorname{some}(\operatorname{eraseNone} s) = s \setminus \{\operatorname{none}\} $$

Finset.insertNone_eraseNone theorem

[DecidableEq (Option α)] (s : Finset (Option α)) : insertNone (eraseNone s) = insert none s

Full source

@[simp]
theorem insertNone_eraseNone [DecidableEq (Option α)] (s : Finset (Option α)) :
    insertNone (eraseNone s) = insert none s := by ext (_ | x) <;> simp

InsertNone-EraseNone Identity: $\operatorname{insertNone}(\operatorname{eraseNone} s) = \{\operatorname{none}\} \cup s$

Informal description

For any finite set $s$ of elements of type $\operatorname{Option} \alpha$ (with decidable equality), the operation $\operatorname{insertNone}$ applied to $\operatorname{eraseNone} s$ equals the insertion of $\operatorname{none}$ into $s$. That is, $\operatorname{insertNone}(\operatorname{eraseNone} s) = \{\operatorname{none}\} \cup s$.

Finset.eraseNone_insertNone theorem

(s : Finset α) : eraseNone (insertNone s) = s

Full source

@[simp]
theorem eraseNone_insertNone (s : Finset α) : eraseNone (insertNone s) = s := by
  ext
  simp

$\operatorname{eraseNone} \circ \operatorname{insertNone}$ is the identity on finite sets

Informal description

For any finite set $s$ of elements of type $\alpha$, the operation of first lifting $s$ to a finite set of $\operatorname{Option} \alpha$ by inserting $\operatorname{none}$ and then removing all $\operatorname{none}$ elements results in the original set $s$. In other words, $\operatorname{eraseNone}(\operatorname{insertNone}(s)) = s$.

Tags