Finset.card_Iic_finset
theorem Finset.card_Iic_finset :
∀ {α : Type u_1} [inst : DecidableEq α] {s : Finset α}, (Finset.Iic s).card = 2 ^ s.card
The theorem `Finset.card_Iic_finset` states that for any type `α` with decidable equality and any finite set `s` of that type, the cardinality (or size) of the set of all elements less than or equal to `s` (denoted `Finset.Iic s`) is equal to 2 to the power of the cardinality of `s` (expressed as `2 ^ s.card` in Lean 4). In other words, the size of the set of all subsets of `s` (including `s` itself) is `2^n`, where `n` is the size of `s`.
More concisely: The cardinality of the interval `[min s : α] to max s : α] (denoted `Finset.Iic s` in Lean 4) of a finite type `α` with decidable equality is equal to 2 raised to the power of the cardinality of `s`.
|
Finset.card_Ico_finset
theorem Finset.card_Ico_finset :
∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α},
s ⊆ t → (Finset.Ico s t).card = 2 ^ (t.card - s.card) - 1
This theorem states that for any given type `α` with decidable equality, and any two finsets `s` and `t` of this type such that `s` is a subset of `t`, the cardinality (or size) of the interval `Finset.Ico s t` (which is the set of all finsets `x` such that `s` is less than or equal to `x` and `x` is strictly less than `t`) is equal to `2` raised to the power of the difference in the cardinalities of `t` and `s`, minus `1`.
More concisely: For any decidably equal type `α` and finsets `s` and `t` of `α` with `s` a subset of `t`, the cardinality of `Finset.Ico s t` is 2^(|t| - |s|), where |.| denotes set size.
|
Finset.card_Ioc_finset
theorem Finset.card_Ioc_finset :
∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α},
s ⊆ t → (Finset.Ioc s t).card = 2 ^ (t.card - s.card) - 1
This theorem is about the cardinality, or the number of elements, in a specific kind of finset. It states that for any type `α` with decidable equality and any two finsets `s` and `t` of this type where `s` is a subset of `t`, the cardinality of the interval of finsets from `s` to `t` - denoted `Finset.Ioc s t` - is equal to 2 raised to the power of the difference between the cardinality of `t` and `s`, minus 1. This can be represented mathematically as: `|Finset.Ioc s t| = 2^(|t| - |s|) - 1`, where `|.|` denotes cardinality.
More concisely: The cardinality of the interval of a finset equals 2 raised to the power of the difference between the cardinalities of the larger and smaller finsets, minus one.
|
Finset.card_Icc_finset
theorem Finset.card_Icc_finset :
∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α}, s ⊆ t → (Finset.Icc s t).card = 2 ^ (t.card - s.card)
This theorem states that for any type `α` with decidable equality, given two finite sets `s` and `t` of type `α` where `s` is a subset of `t`, the cardinality (i.e., the number of elements) of the closed interval between `s` and `t` in the finite set sense is equal to `2` to the power of the difference between the cardinalities of `t` and `s`. In other words, if you have two finite sets where one is a subset of the other, there are `2` to the power of the difference in their sizes number of sets between them, including the two sets themselves.
More concisely: For finite sets `s` and `t` of type `α` with decidable equality, the cardinality of the closed interval between `s` and `t` is 2 raised to the power of the cardinality difference between `t` and `s`.
|
Finset.card_Iio_finset
theorem Finset.card_Iio_finset :
∀ {α : Type u_1} [inst : DecidableEq α] {s : Finset α}, (Finset.Iio s).card = 2 ^ s.card - 1
This theorem states that for any given type `α` with decidable equality and any given finite set of elements of type `α`, the cardinality (or the number of elements) of the set of elements less than each element in the original set (denoted as `Finset.Iio s`) is equal to `2` raised to the power of the cardinality of the original set, subtracted by `1`. In mathematical terms, if `s` is a finite set, then the number of elements in the set of elements that are less than each element in `s` is `2` to the power of the number of elements in `s`, minus `1`.
More concisely: For any finite type `α` with decidable equality, the number of elements less than each element in a finite set `s` of type `α` is 2^|s| - 1.
|
Finset.strictMono_iff_forall_lt_cons
theorem Finset.strictMono_iff_forall_lt_cons :
∀ {α : Type u_1} {β : Type u_2} [inst : Preorder β] {f : Finset α → β},
StrictMono f ↔ ∀ (s : Finset α) ⦃a : α⦄ (ha : a ∉ s), f s < f (Finset.cons a s ha)
The theorem `Finset.strictMono_iff_forall_lt_cons` states that for any two types `α` and `β`, given a preorder on `β`, and a function `f` mapping from `Finset α` to `β`, `f` is strictly monotone if and only if for all finite sets `s` of type `α` and for all `a` of type `α` not in `s`, the value of `f` at `s` is strictly less than the value of `f` at the finite set obtained by adding `a` to `s`. In other words, adding a new element to a set always increases the value of the function `f`.
More concisely: A function `f` from `Finset α` to a preordered type `β` is strictly monotone if and only if for all `s` in `Finset α` and all `a` not in `s`, `f s < f (s.insert a)`.
|
Finset.strictAnti_iff_forall_cons_lt
theorem Finset.strictAnti_iff_forall_cons_lt :
∀ {α : Type u_1} {β : Type u_2} [inst : Preorder β] {f : Finset α → β},
StrictAnti f ↔ ∀ (s : Finset α) ⦃a : α⦄ (ha : a ∉ s), f (Finset.cons a s ha) < f s
The theorem `Finset.strictAnti_iff_forall_cons_lt` states that, for all types `α` and `β` where `β` has a preorder structure, a function `f` from a finite set of type `α` to `β` is strictly anti-monotonic, meaning `f` decreases at each step, if and only if for every finite set `s` and an element `a` not in `s`, the function value of the finite set constructed by including `a` in `s` is less than the function value of `s` itself. This finite set is constructed using the `cons` operation which adds an element `a` to `s` without the need of `a` being decidable equal and ensures the union is distinct.
More concisely: A function from a finite set to a preordered type is strictly anti-monotonic if and only if appending an element not in the set strictly decreases the function value.
|
Finset.monotone_iff_forall_le_insert
theorem Finset.monotone_iff_forall_le_insert :
∀ {α : Type u_1} {β : Type u_2} [inst : Preorder β] {f : Finset α → β} [inst_1 : DecidableEq α],
Monotone f ↔ ∀ (s : Finset α) ⦃a : α⦄, a ∉ s → f s ≤ f (insert a s)
The theorem `Finset.monotone_iff_forall_le_insert` establishes an equivalence condition for a function `f` from a finite set (`Finset α`) to be monotone in the context of preordered type `β`. Specifically, it states that a function `f` is monotone if and only if for all finite sets `s` and all elements `a` not in `s`, the value of `f` at `s` is less than or equal to the value of `f` at the set obtained by inserting `a` into `s`. The condition is applicable when the equality in type `α` is decidable.
More concisely: A function from a finite set to a preordered type is monotone if and only if for all elements not in the set, the function value at the set is less than or equal to the function value at the set with that element inserted.
|
Finset.antitone_iff_forall_cons_le
theorem Finset.antitone_iff_forall_cons_le :
∀ {α : Type u_1} {β : Type u_2} [inst : Preorder β] {f : Finset α → β},
Antitone f ↔ ∀ (s : Finset α) ⦃a : α⦄ (ha : a ∉ s), f (Finset.cons a s ha) ≤ f s
The theorem `Finset.antitone_iff_forall_cons_le` states that for all types `α` and `β`, given a preorder on `β`, a function `f` from `Finset α` to `β` is antitone (i.e., for all `a` and `b` in the domain, if `a ≤ b` then `f(b) ≤ f(a)`) if and only if for all finsets `s` of `α` and all `a` in `α` not in `s`, `f` of the finset resulting from adding `a` to `s` is less than or equal to `f` of `s`. This means that adding an element to the finset doesn't increase the value of the function, thus making it decreasing or remaining constant.
More concisely: A function from a finite set to a preordered type is antitone if and only if adding any element not in the set does not cause an increase in the function value.
|
Finset.strictMono_iff_forall_lt_insert
theorem Finset.strictMono_iff_forall_lt_insert :
∀ {α : Type u_1} {β : Type u_2} [inst : Preorder β] {f : Finset α → β} [inst_1 : DecidableEq α],
StrictMono f ↔ ∀ (s : Finset α) ⦃a : α⦄, a ∉ s → f s < f (insert a s)
The theorem `Finset.strictMono_iff_forall_lt_insert` states that for any types `α` and `β`, where `β` has a preorder structure and `α` has decidable equality, a function `f` that maps a finite set of elements of type `α` to `β` is strictly monotone if and only if for any finite set `s` and any element `a` of type `α` not in `s`, the value of `f` at `s` is less than the value of `f` at the finite set obtained by inserting `a` into `s`. In other words, adding a new distinct element to the set always increases the value of the function `f`.
More concisely: A function from a finite set of decidably equal types to a preordered type is strictly monotone if and only if adding any new distinct element to the set strictly increases the function value.
|
Finset.card_Ioo_finset
theorem Finset.card_Ioo_finset :
∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α},
s ⊆ t → (Finset.Ioo s t).card = 2 ^ (t.card - s.card) - 2
The theorem `Finset.card_Ioo_finset` states that for any type `α` with decidable equality and any two finite sets `s` and `t` of this type, if `s` is a subset of `t`, then the cardinality of the set of elements `x` such that `s < x` and `x < t` is equal to `2` to the power of (the cardinality of `t` minus the cardinality of `s`) minus `2`. This theorem essentially quantifies the number of sets strictly between two given finite sets.
More concisely: For finite sets `s` and `t` of type `α` with decidable equality, if `s` is a subset of `t`, then the number of elements `x` in `α` such that `s < x` and `x < t` is equal to 2^(card `t` - card `s` - 1).
|
Finset.antitone_iff_forall_insert_le
theorem Finset.antitone_iff_forall_insert_le :
∀ {α : Type u_1} {β : Type u_2} [inst : Preorder β] {f : Finset α → β} [inst_1 : DecidableEq α],
Antitone f ↔ ∀ (s : Finset α) ⦃a : α⦄, a ∉ s → f (insert a s) ≤ f s
This theorem is stating that a function `f` from `Finset α` to `β` is antitone (for all `a` and `b`, if `a ≤ b` then `f(b) ≤ f(a)`) if and only if for all sets `s` and elements `a` not in `s`, the value of `f` at the set obtained by inserting `a` into `s` is less than or equal to the value of `f` at `s`. Here, `α` and `β` are types with `β` having a preorder structure, and `α` having decidable equality.
More concisely: A function `f` from a finite set `α` to a preordered type `β` is antitone if and only if for all sets `s` and elements `a` not in `s`, `f(s : Finset α ++ {a}) ≤ f s`, where `++` denotes set union and `Finset α` is the type of finite sets of `α`.
|
Finset.strictAnti_iff_forall_lt_insert
theorem Finset.strictAnti_iff_forall_lt_insert :
∀ {α : Type u_1} {β : Type u_2} [inst : Preorder β] {f : Finset α → β} [inst_1 : DecidableEq α],
StrictAnti f ↔ ∀ (s : Finset α) ⦃a : α⦄, a ∉ s → f (insert a s) < f s
The theorem `Finset.strictAnti_iff_forall_lt_insert` states that for every type `α`, and for another type `β` which has a preorder relation, a function `f` from `Finset α` to `β` is strictly antitone if and only if for all `s` in `Finset α` and for all `a` in `α`, if `a` is not an element of `s`, then the value of function `f` at the insertion of `a` into `s` is less than the value of function `f` at `s`. This theorem requires that the equality for elements in `α` is decidable.
More concisely: For any type `α` and preorder `β`, a function `f` from `Finset α` to `β` is strictly antitone if and only if for all `s` in `Finset α` and all `a` not in `s`, `f(s.insert a) < f s`.
|
Finset.monotone_iff_forall_le_cons
theorem Finset.monotone_iff_forall_le_cons :
∀ {α : Type u_1} {β : Type u_2} [inst : Preorder β] {f : Finset α → β},
Monotone f ↔ ∀ (s : Finset α) ⦃a : α⦄ (ha : a ∉ s), f s ≤ f (Finset.cons a s ha)
A function `f` mapping from a finite set `α` to `β` is defined to be monotone under a preorder relationship on `β` if and only if for any finite set `s` and any element `a` that does not belong to `s`, the value of `f` at `s` is less than or equal to the value of `f` at the set formed by adding `a` to `s` (`cons a s ha`).
More concisely: A function from a finite set to another set is monotone with respect to a preorder if and only if for all finite sets `s` and elements `a not in s`, `f(s) ≤ f(s : set α ++ {a})`.
|