Mathlib.Data.Finset.Option._auxLemma.5
theorem Mathlib.Data.Finset.Option._auxLemma.5 :
∀ {α : Type u_1} {s : Finset (Option α)} {x : α}, (x ∈ Finset.eraseNone s) = (some x ∈ s)
The theorem `Mathlib.Data.Finset.Option._auxLemma.5` states that for any type `α`, any finite set `s` of optional values of type `α`, and any value `x` of type `α`, `x` belongs to the set obtained by erasing `None` values from `s` if and only if `Some x` belongs to `s`. In other words, this theorem is saying that an element is in the set derived from `s` by removing `None` values precisely when its `Some` version is in the original set `s`.
More concisely: For any type `α` and finite set `s` of optional values `α`, an element `x` belongs to the set `s` without its `None` values if and only if `Some x` belongs to `s`.
|
Finset.insertNone.proof_1
theorem Finset.insertNone.proof_1 : ∀ {α : Type u_1} (s : Finset α), none ∉ Finset.map Function.Embedding.some s := by
sorry
This theorem states that, for any type `α` and any finite set `s` of type `α`, the `None` value is not an element of the image of `s` under the embedding using the `some` function. In other words, when we embed each element of a finite set into the `Option α` type by wrapping it with the `Some` constructor, the `None` value is guaranteed to not be in the resulting set.
More concisely: For any finite set `s` and type `α`, the image of `s` under the embedding using the `some` function is a subset of `Option α \ {None}`.
|
Finset.mem_eraseNone
theorem Finset.mem_eraseNone : ∀ {α : Type u_1} {s : Finset (Option α)} {x : α}, x ∈ Finset.eraseNone s ↔ some x ∈ s
This theorem states that for any type `α`, any set `s` of optional elements of type `α`, and any element `x` of type `α`, the element `x` is a member of the set obtained by erasing all `None` options from `s` if and only if `Some x`, i.e., the option holding `x`, is an element of `s`. In other words, `Finset.eraseNone` effectively removes all `None` options from the set `s`, and an element `x` exists in the resulting set if and only if `x` was originally in `s` as an optional value.
More concisely: For any type `α` and set `s` of optional elements of type `α`, an element `x` is in the set `Finset.eraseNone s` if and only if `Some x` is in `s`.
|
Mathlib.Data.Finset.Option._auxLemma.2
theorem Mathlib.Data.Finset.Option._auxLemma.2 : ∀ {α : Type u_1} {a : α} {o : Option α}, (a ∈ o.toFinset) = (a ∈ o)
This theorem states that for any type `α`, any element `a` of type `α`, and any optional value `o` of type `α`, the statement "element `a` is a member of the set obtained by converting the optional value `o` to a finite set" is equivalent to the statement "element `a` is present in the optional value `o`".
More concisely: For any type `α`, element `a` of `α`, and optional value `o` of type `option α`, `a ∈ set o` if and only if `a = some a' ∈ o` for some `a'`.
|
Mathlib.Data.Finset.Option._auxLemma.3
theorem Mathlib.Data.Finset.Option._auxLemma.3 :
∀ {α : Type u_1} {s : Finset α} {o : Option α}, (o ∈ Finset.insertNone s) = ∀ a ∈ o, a ∈ s
This theorem states that for any type `α`, any finite set `s` of elements of type `α`, and any `Option α` (which is either `Some a` for some `a` of type `α` or `None`), `o` belongs to the finite set obtained from `s` by applying `Finset.insertNone` if and only if for every element `a` in `o` (`a` is `None` or `Some value`), `a` belongs to `s`. In other words, an option `o` is in the result of inserting `None` into `s` and lifting `s` to `Option α` if and only if every element in `o` is in `s`.
More concisely: For any type `α`, a finite set `s` of elements from `α`, and an `Option α`, the option belongs to the finite set obtained by inserting `None` into `s` if and only if all elements in the option are in `s`.
|