Finset.mem_upShadow_iff_erase_mem
theorem Finset.mem_upShadow_iff_erase_mem :
∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {𝒜 : Finset (Finset α)} {t : Finset α},
t ∈ 𝒜.upShadow ↔ ∃ a ∈ t, t.erase a ∈ 𝒜
The theorem `Finset.mem_upShadow_iff_erase_mem` states that for any type `α` with decidable equality and which is a finite type, any finset `𝒜` of finsets of `α`, and any finset `t` of `α`, `t` is in the upper shadow of `𝒜` if and only if there exists an element `a` in `t` such that the finset resulting from erasing `a` from `t` is in `𝒜`. In other words, a finset `t` is in the upper shadow of a set of finsets `𝒜` precisely when we can remove one element from `t` to get a finset that is a member of `𝒜`.
More concisely: For any finite type `α` with decidable equality, a finset `t` of `α` is in the upper shadow of a finset of finsets `𝒜` of `α` if and only if there exists an element `a` in `t` such that the finset obtained by erasing `a` from `t` is in `𝒜`.
|
Finset.exists_subset_of_mem_shadow
theorem Finset.exists_subset_of_mem_shadow :
∀ {α : Type u_1} [inst : DecidableEq α] {𝒜 : Finset (Finset α)} {t : Finset α}, t ∈ 𝒜.shadow → ∃ s ∈ 𝒜, t ⊆ s := by
sorry
This theorem states that for any type `α` with decidable equality and for any finite sets `𝒜` and `t` of type `α`, if `t` is in the shadow of `𝒜`, there exists a subset `s` that belongs to `𝒜` and `t` is a subset of `s`. In other words, being in the shadow of `𝒜` implies that we can find a superset of `t` within `𝒜`.
More concisely: For any decidably equal type `α` and finite sets `𝒜` and `t` of type `α`, if `t` is in the shadow of `𝒜`, then there exists a subset `s` in `𝒜` such that `t` is a subset of `s`.
|
Finset.mem_upShadow_iterate_iff_exists_mem_card_add
theorem Finset.mem_upShadow_iterate_iff_exists_mem_card_add :
∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {𝒜 : Finset (Finset α)} {t : Finset α} {k : ℕ},
t ∈ Finset.upShadow^[k] 𝒜 ↔ ∃ s ∈ 𝒜, s ⊆ t ∧ t.card = s.card + k
The theorem `Finset.mem_upShadow_iterate_iff_exists_mem_card_add` states that for any type `α` with decidable equality and finite number of elements, given a family of sets `𝒜` of type `α`, a set `t` of type `α`, and a natural number `k`, `t` belongs to the `k`-times iterated upper shadow of `𝒜` if and only if there exists some set `s` in `𝒜` such that `s` is a subset of `t` and the cardinality of `t` is equal to the cardinality of `s` plus `k`. This means that `t` can be obtained by adding exactly `k` elements to some set in `𝒜`.
More concisely: For any type `α` with decidable equality and finite number of elements, a set `t` belongs to the `k`-times iterated upper shadow of a family of sets `𝒜` if and only if there exists a set `s` in `𝒜` such that `s` is a subset of `t` and the cardinality of `t` equals the cardinality of `s` plus `k`.
|
Mathlib.Combinatorics.SetFamily.Shadow._auxLemma.3
theorem Mathlib.Combinatorics.SetFamily.Shadow._auxLemma.3 :
∀ {α : Type u_1} [inst : DecidableEq α] {𝒜 : Finset (Finset α)} {t : Finset α},
(t ∈ 𝒜.shadow) = ∃ s ∈ 𝒜, ∃ a ∈ s, s.erase a = t
This theorem states that for any type `α` with decidable equality, any family of finite sets `𝒜`, and any set `t` of type `α`, `t` is in the shadow of `𝒜` if and only if there exists a set `s` in `𝒜` and an element `a` in `s` such that `t` is the set `s` with the element `a` removed. In other words, the shadow of a set family `𝒜` can be characterized as all sets that can be obtained by removing one element from a set in `𝒜`.
More concisely: For any decidably equal type `α` and family `𝒜` of finite sets, a set `t` is in the shadow of `𝒜` if and only if there exists `s ∈ 𝒜` and `a ∈ s` such that `t = s \ {a}`.
|
Finset.mem_shadow_iff
theorem Finset.mem_shadow_iff :
∀ {α : Type u_1} [inst : DecidableEq α] {𝒜 : Finset (Finset α)} {t : Finset α},
t ∈ 𝒜.shadow ↔ ∃ s ∈ 𝒜, ∃ a ∈ s, s.erase a = t
The theorem `Finset.mem_shadow_iff` states for any type `α` with decidable equality, and any two finite sets `𝒜` and `t` of type `α`, `t` is in the shadow of `𝒜` if and only if there exists a finite set `s` in `𝒜` such that we can find an element `a` in `s` which, when removed from `s`, yields `t`. Here, the shadow of a set `𝒜` is defined as the set of all possible subsets that can be obtained by removing one element from any subset in `𝒜`.
More concisely: A finite set `t` is in the shadow of a finite set `𝒜` if and only if there exists a set `s` in `𝒜` from which `t` can be obtained by removing one element.
|
Set.Sized.shadow_iterate
theorem Set.Sized.shadow_iterate :
∀ {α : Type u_1} [inst : DecidableEq α] {𝒜 : Finset (Finset α)} {k r : ℕ},
Set.Sized r ↑𝒜 → Set.Sized (r - k) ↑(Finset.shadow^[k] 𝒜)
The theorem `Set.Sized.shadow_iterate` states that for any type `α` with a decidable equality relation, given a `k`, `r`, and a finite set of finite sets `𝒜` (representing a family of sets), if every set in `𝒜` has size `r` (i.e., `𝒜` is an `r`-set family), then after applying the `k`-th iteration of the "shadow" operation to `𝒜`, we obtain a new set family where every set has size `r - k` (i.e., the `k`-th shadow of `𝒜` is an `(r - k)`-set family).
In other words, applying the "shadow" operation `k` times to a family of `r`-sets results in a family of `(r - k)`-sets. The "shadow" operation here refers to the process of obtaining a new set family by removing one element from each set in the original set family.
More concisely: For any decidably equal type `α` and finite set of finite sets `𝒜` with each set having size `r`, the `k`-th iteration of the "shadow" operation on `𝒜` results in a new family of sets, each having size `r - k`.
|
Finset.upShadow_monotone
theorem Finset.upShadow_monotone :
∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α], Monotone Finset.upShadow
This theorem states that the upper shadow function on finite sets is monotone. In other words, if we have a type `α` with a decidable equality and a finite number of instances, then if we have two set families `𝒜` and `` such that `𝒜` is a subset of ``, the upper shadow of `𝒜` is also a subset of the upper shadow of ``. Here, the "upper shadow" of a set family is defined as the collection of all sets we can obtain by adding one element to any set in the original family.
More concisely: If `α` is a type with decidable equality and finitely many instances, and `𝒜` is a subset of ``, then the upper shadow of `𝒜` is included in the upper shadow of ``.
|
Mathlib.Combinatorics.SetFamily.Shadow._auxLemma.13
theorem Mathlib.Combinatorics.SetFamily.Shadow._auxLemma.13 :
∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {𝒜 : Finset (Finset α)} {t : Finset α},
(t ∈ 𝒜.upShadow) = ∃ s ∈ 𝒜, ∃ a ∉ s, insert a s = t
The theorem `_auxLemma.13` in the `Mathlib.Combinatorics.SetFamily.Shadow` namespace states that for any type `α` with decidable equality and finite number of instances, and for any set of sets `𝒜` and set `t` of type `α`, `t` belongs to the upper shadow of `𝒜` if and only if there exists a set `s` in `𝒜` and an element `a` not in `s` such that inserting `a` into `s` yields `t`. The upper shadow of a set family `𝒜` is all sets we can get by adding one element to any set in `𝒜`.
More concisely: For any type `α` with decidable equality and finite number of instances, and any set family `𝒜` and set `t` of type `α`, `t` is in the upper shadow of `𝒜` if and only if there exists a set `s` in `𝒜` and an element `a` not in `s` such that `t = s ∪ {a}`.
|
Set.Sized.shadow
theorem Set.Sized.shadow :
∀ {α : Type u_1} [inst : DecidableEq α] {𝒜 : Finset (Finset α)} {r : ℕ},
Set.Sized r ↑𝒜 → Set.Sized (r - 1) ↑𝒜.shadow
This theorem states that for any type `α` with decidable equality and given a family `𝒜` of finite sets of `α`, if every set in `𝒜` has size `r`, then every set in the shadow of `𝒜` (which is obtained by removing an element from each set in `𝒜`) will have size `r - 1`. In other words, if `𝒜` is a family of `r`-sets, then its shadow is a family of `(r - 1)`-sets.
More concisely: Given a family `𝒜` of finite sets of type `α` with decidable equality, if every set in `𝒜` has size `r`, then every set in the shadow of `𝒜` has size `r - 1`.
|
Finset.mem_upShadow_iff_exists_sdiff
theorem Finset.mem_upShadow_iff_exists_sdiff :
∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {𝒜 : Finset (Finset α)} {t : Finset α},
t ∈ 𝒜.upShadow ↔ ∃ s ∈ 𝒜, s ⊆ t ∧ (t \ s).card = 1
The theorem `Finset.mem_upShadow_iff_exists_sdiff` states that for any arbitrary type `α` with a decidable equality and finiteness, a given finite set `t` of type `α` belongs to the upper shadow of a finite set `𝒜` of finite sets of type `α` if and only if there exists a subset `s` in `𝒜` such that `s` is a subset of `t` and the cardinality of the set difference `t \ s` is exactly one. In other words, `t` is one element larger than some set from `𝒜`.
The term "upper shadow" is used in combinatorics to denote the set of all sets that can be obtained by adding one element to a given set, and `𝒜.upShadow` represents the upper shadow of the finite set `𝒜`. The symbol `\` denotes set difference and `card` computes the cardinality of a set. The `DecidableEq α` and `Fintype α` type class instances ensure that equality is decidable and the type is finite, respectively.
More concisely: A finite set belongs to the upper shadow of a finite set of finite sets if and only if it is one element larger than some set in that collection.
|
Finset.mem_shadow_iterate_iff_exists_mem_card_add
theorem Finset.mem_shadow_iterate_iff_exists_mem_card_add :
∀ {α : Type u_1} [inst : DecidableEq α] {𝒜 : Finset (Finset α)} {t : Finset α} {k : ℕ},
t ∈ Finset.shadow^[k] 𝒜 ↔ ∃ s ∈ 𝒜, t ⊆ s ∧ s.card = t.card + k
This theorem states that, for any given type `α` with decidable equality, a given set family `𝒜` which is a finite set of finite sets of `α`, a set `t` of `α`, and a natural number `k`, `t` is in the `k`-times iterated shadow of `𝒜` if and only if there exists a set `s` in `𝒜` such that `t` is a subset of `s` and the cardinality of `s` is `k` more than the cardinality of `t`.
Here, the `k`-times iterated shadow of `𝒜` is the set of all sets we can get by removing `k` elements from any set in `𝒜`. Thus, the theorem connects the concept of shadow of a set with the subset relation and cardinalities of sets.
More concisely: For any decidably equal type `α`, finite set family `𝒜` of finite sets of `α`, set `t` of `α`, and natural number `k`, `t` is in the `k`-times iterated shadow of `𝒜` if and only if there exists an `s` in `𝒜` such that `t` is a subset of `s` and the cardinality of `s` is `k` greater than that of `t`.
|
Finset.mem_upShadow_iff
theorem Finset.mem_upShadow_iff :
∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {𝒜 : Finset (Finset α)} {t : Finset α},
t ∈ 𝒜.upShadow ↔ ∃ s ∈ 𝒜, ∃ a ∉ s, insert a s = t
The theorem states that for any given type `α` with decidable equality and a pre-defined size, a finset `t` of `α` is in the upper shadow of another finset `𝒜` if and only if there exists an element `s` in `𝒜` such that we can find an element `a` not in `s`, and adding `a` to `s` results in the finset `t`. Here, `𝒜` and `t` are both finsets of `α`, and `𝒜.upShadow` represents the set of all finsets that can be obtained by adding an element to a finset in `𝒜`.
More concisely: For any decidably equated type `α` with defined size, finset `t` is in the upper shadow of finset `𝒜` if and only if there exists an element `s` in `𝒜` such that `t = s.toFinset ++ {a}| a ∈ α \ s`.
|
Set.Sized.upShadow
theorem Set.Sized.upShadow :
∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {𝒜 : Finset (Finset α)} {r : ℕ},
Set.Sized r ↑𝒜 → Set.Sized (r + 1) ↑𝒜.upShadow
This theorem states that the upper shadow of a family of sets, where each set has `r` elements, is a family of sets where each set has `r + 1` elements. Here, `𝒜` denotes a family of sets, and `upShadow` is a function in Lean that returns the upper shadow of a family of sets. The upper shadow of a family of sets is defined as the collection of all sets that can be obtained by adding one element to a set in the family. The theorem holds for any type `α` with decidable equality and any such `α` that is a finite type.
More concisely: For any family `𝒜` of finite sets of type `α` with `r` elements each, the upper shadow of `𝒜` is a family of sets of type `α` with `r + 1` elements each.
|
Finset.mem_shadow_iff_exists_mem_card_add_one
theorem Finset.mem_shadow_iff_exists_mem_card_add_one :
∀ {α : Type u_1} [inst : DecidableEq α] {𝒜 : Finset (Finset α)} {t : Finset α},
t ∈ 𝒜.shadow ↔ ∃ s ∈ 𝒜, t ⊆ s ∧ s.card = t.card + 1
This theorem, `Finset.mem_shadow_iff_exists_mem_card_add_one`, says that for any type `α` with a decidable equality relation, for any finite set of finite sets `𝒜`, and for any finite set `t`, `t` is in the shadow of `𝒜` if and only if there exists a set `s` in `𝒜` such that `t` is a subset of `s` and the cardinality of `s` is one greater than the cardinality of `t`. In other words, `t` is in the shadow of `𝒜` if `t` is missing exactly one element from a set in `𝒜`.
More concisely: A finite set `t` is in the shadow of a finite set of finite sets `𝒜` if and only if there exists a set `s` in `𝒜` such that `t` is a subset of `s` and the cardinality of `s` is one larger than that of `t`.
|
Finset.shadow_empty
theorem Finset.shadow_empty : ∀ {α : Type u_1} [inst : DecidableEq α], ∅.shadow = ∅
This theorem states that the "shadow" of the empty set is also an empty set, given any type `α` that has a decidable equality. In other words, for any type `α` for which we can decide whether two elements are equal, the shadow operation (which is a specific operation in the context of Finite sets or `Finset` in Lean 4) applied to the empty set results in another empty set.
More concisely: For any type `α` with decidable equality, the shadow of the empty `Finset α` is the empty `Finset α`.
|
Finset.shadow_monotone
theorem Finset.shadow_monotone : ∀ {α : Type u_1} [inst : DecidableEq α], Monotone Finset.shadow
The theorem `Finset.shadow_monotone` asserts that the operation of taking the shadow of a set is a monotone function. In other words, if we have a type `α` with decidable equality, for any two set families `𝒜` and `` of type `Finset (Finset α)`, if `𝒜 ≤ ` (i.e., every set in `𝒜` is also in ``), then the shadow of `𝒜` is also less than or equal to the shadow of ``. Here, the shadow of a set family is defined as the collection of all sets that can be obtained by removing one element from any set in the original family.
More concisely: If `α` has decidable equality and `𝒜` is a subset of `` (i.e., every set in `𝒜` is in ``), then the collection of sets obtained by removing one element from each set in `𝒜` (the shadow of `𝒜`) is contained in the collection of sets obtained by removing one element from each set in `` (the shadow of ``).
|
Finset.mem_shadow_iterate_iff_exists_sdiff
theorem Finset.mem_shadow_iterate_iff_exists_sdiff :
∀ {α : Type u_1} [inst : DecidableEq α] {𝒜 : Finset (Finset α)} {t : Finset α} {k : ℕ},
t ∈ Finset.shadow^[k] 𝒜 ↔ ∃ s ∈ 𝒜, t ⊆ s ∧ (s \ t).card = k
This theorem states that a set `t` belongs to the k-times iterated shadow of a family of sets `𝒜`, denoted as `∂^k 𝒜`, if and only if there exists a set `s` in `𝒜` such that `t` is a subset of `s` and the cardinality of the set difference `s \ t` is exactly `k`. In other words, it means that `t` can be obtained from a set in `𝒜` by removing exactly `k` elements. This theorem is a part of `Finset.mem_shadow_iterate_iff_exists_sdiff` in Lean 4.
More concisely: A set belongs to the k-times iterated shadow of a family of sets if and only if there exists a set in the family whose difference with the set has cardinality equal to k.
|
Finset.mem_upShadow_iterate_iff_exists_sdiff
theorem Finset.mem_upShadow_iterate_iff_exists_sdiff :
∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {𝒜 : Finset (Finset α)} {t : Finset α} {k : ℕ},
t ∈ Finset.upShadow^[k] 𝒜 ↔ ∃ s ∈ 𝒜, s ⊆ t ∧ (t \ s).card = k
The theorem `Finset.mem_upShadow_iterate_iff_exists_sdiff` states that for any given type `α` with decidable equality and finiteness, a set of sets `𝒜`, a set `t`, and a natural number `k`, `t` is in the `k`-iterated upper shadow of `𝒜` if and only if there exists a set `s` in `𝒜` such that `s` is a subset of `t` and the cardinality of the set difference between `t` and `s` is exactly `k`. This means `t` can be obtained by adding `k` elements to some set `s` from `𝒜`.
More concisely: For any type `α` with decidable equality and finiteness, set `𝒜`, natural number `k`, and `t`, `t` is in the `k`-iterated upper shadow of `𝒜` if and only if there exists `s` in `𝒜` such that `s` is a subset of `t` and `|t \ s| = k`.
|
Finset.exists_subset_of_mem_upShadow
theorem Finset.exists_subset_of_mem_upShadow :
∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {𝒜 : Finset (Finset α)} {s : Finset α},
s ∈ 𝒜.upShadow → ∃ t ∈ 𝒜, t ⊆ s
The theorem `Finset.exists_subset_of_mem_upShadow` states that for any type `α` with decidable equality and is a finite type, given a finite set `𝒜` of finite sets of `α` and another finite set `s` of `α`, if `s` is in the upper shadow of `𝒜` (denoted by `𝒜.upShadow`), then there exists a set `t` in `𝒜` that is a subset of `s`. In other words, being in the upper shadow of `𝒜` implies that `s` has a superset in `𝒜`.
More concisely: If `α` is a finite type with decidable equality, `𝒜` is a finite set of finite sets of `α`, and `s` is a finite set of `α` in the upper shadow of `𝒜`, then there exists a set `t` in `𝒜` such that `t ⊆ s`.
|
Finset.mem_shadow_iff_exists_sdiff
theorem Finset.mem_shadow_iff_exists_sdiff :
∀ {α : Type u_1} [inst : DecidableEq α] {𝒜 : Finset (Finset α)} {t : Finset α},
t ∈ 𝒜.shadow ↔ ∃ s ∈ 𝒜, t ⊆ s ∧ (s \ t).card = 1
This theorem states that a set `t` is in the shadow of a finset `𝒜` if and only if there exists another set `s` in `𝒜` such that `t` is a subset of `s` and the cardinality (size) of the set difference `s \ t` (elements in `s` but not in `t`) is exactly one. This is all in the context where the type `α` has decidable equality. In other words, `t` is in the shadow of `𝒜` if it can be obtained from a set in `𝒜` by removing exactly one element. The shadow of a finset is a concept used in combinatorics.
More concisely: A set `t` is in the shadow of a finset `𝒜` if and only if there exists a set `s` in `𝒜` such that `t` is a subset of `s` and the cardinality difference of `s` and `t` equals one.
|
Finset.mem_shadow_iff_insert_mem
theorem Finset.mem_shadow_iff_insert_mem :
∀ {α : Type u_1} [inst : DecidableEq α] {𝒜 : Finset (Finset α)} {t : Finset α},
t ∈ 𝒜.shadow ↔ ∃ a ∉ t, insert a t ∈ 𝒜
The theorem `Finset.mem_shadow_iff_insert_mem` states that for any type `α` with a decidable equality relation, a set `𝒜` of finite sets of `α`, and a finite set `t` of `α`, `t` is in the shadow of `𝒜` if and only if there exists an element `a` not in `t` such that adding this element `a` to `t` results in a set that is in `𝒜`. In other words, a finset `t` is considered to be in the shadow of a larger finset `𝒜` if we can add an element to `t`, not already in `t`, to obtain a finset that is a member of `𝒜`.
More concisely: For any type `α` with decidable equality and a set `𝒜` of finite sets of `α`, a finite set `t` is in the shadow of `𝒜` if and only if there exists an `a ∈ α \ t` such that `t ∪ {a} ∈ 𝒜`.
|
Finset.upShadow_empty
theorem Finset.upShadow_empty : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α], ∅.upShadow = ∅
This theorem states that the upper shadow of the empty set is itself an empty set. Here, the upper shadow of a set is a concept from combinatorics. The theorem is applicable for any type `α`, given that `α` has a decidable equality (i.e., for any two elements of `α`, it can be decided whether they are equal or not) and is a finite type (i.e., `α` has a finite number of distinct values).
More concisely: The upper shadow of the empty set is an empty set for any type `α` with decidable equality and finite number of elements.
|
Finset.mem_upShadow_iff_exists_mem_card_add_one
theorem Finset.mem_upShadow_iff_exists_mem_card_add_one :
∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {𝒜 : Finset (Finset α)} {t : Finset α},
t ∈ 𝒜.upShadow ↔ ∃ s ∈ 𝒜, s ⊆ t ∧ t.card = s.card + 1
This theorem states that for any type `α` with decidable equality and finite number of elements, a given set `t` belongs to the upper shadow of a family of sets `𝒜` if and only if there exists a set `s` in `𝒜` such that `s` is a subset of `t` and the cardinality of `t` is exactly one more than the cardinality of `s`. The upper shadow of a family of sets is the collection of all sets that can be obtained by adding exactly one element to a set in the family.
The theorem is also related to `Finset.mem_upShadow_iff_exists_sdiff`, which provides another way of characterizing membership in the upper shadow of a family of sets.
More concisely: For any type `α` with decidable equality and finite number of elements, a set `t` belongs to the upper shadow of a family of sets `𝒜` if and only if there exists a set `s` in `𝒜` such that `s` is a subset of `t` and the cardinality of `t` is one element greater than that of `s`.
|
Mathlib.Combinatorics.SetFamily.Shadow._auxLemma.4
theorem Mathlib.Combinatorics.SetFamily.Shadow._auxLemma.4 :
∀ {α : Type u_1} {s t : Finset α} [inst : DecidableEq α], (t ⊆ s ∧ (s \ t).card = 1) = (t ⋖ s)
This theorem, `Mathlib.Combinatorics.SetFamily.Shadow._auxLemma.4`, states that for any type `α`, and for any finite sets `s` and `t` of type `α` where equality of elements in `α` is decidable, the statement that `t` is a subset of `s` and the cardinality of the set difference `s \ t` is one, is equivalent to `t` being a shadow of `s`. The shadow of a set `s`, denoted `t ⋖ s`, is a concept in combinatorics referring to all sets that can be obtained from `s` by removing one element.
More concisely: For any type `α` with decidable equality and finite sets `s` and `t` of type `α`, `t` being a subset of `s` with cardinality difference equal to one is equivalent to `t` being a shadow of `s`.
|
Finset.mem_upShadow_iff_exists_mem_card_add
theorem Finset.mem_upShadow_iff_exists_mem_card_add :
∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {𝒜 : Finset (Finset α)} {s : Finset α} {k : ℕ},
s ∈ Finset.upShadow^[k] 𝒜 ↔ ∃ t ∈ 𝒜, t ⊆ s ∧ t.card + k = s.card
This theorem states that for any given types `α`, set `𝒜` of finite sets of `α`, set `s` of `α`, and natural number `k`, the set `s` is in the `k`-times iterated upper shadow of `𝒜` if and only if there exists a set `t` in `𝒜` such that `t` is a subset of `s` and the cardinality of `t` plus `k` equals the cardinality of `s`. Here, the `k`-times iterated upper shadow of `𝒜` is the set of all finite sets we can get by adding `k` elements to any set in `𝒜`. This theorem basically describes the condition under which a set is in the `k`-times iterated upper shadow of a set of sets.
More concisely: A set `s` is in the `k`-times iterated upper shadow of a set `𝒜` of finite sets of type `α` if and only if there exists a set `t` in `𝒜` such that `t` is a subset of `s` and the cardinality of `t` plus `k` equals the cardinality of `s`.
|