LeanAide documentation

LeanAide GPT-4 documentation

Module: Mathlib.Data.Finset.Card

`Finset.card_union_add_card_inter` theorem Finset.card_union_add_card_inter : ∀ {α : Type u_1} [inst : DecidableEq α] (s t : Finset α), (s ∪ t).card + (s ∩ t).card = s.card + t.card This theorem states that for any type `α` with a decidable equality relation, and any two finite sets `s` and `t` of this type, the cardinality of the union of `s` and `t` plus the cardinality of the intersection of `s` and `t` is equal to the sum of the cardinalities of `s` and `t`. This is essentially a restatement of the principle of inclusion-exclusion in set theory. More concisely: For any type `α` with decidable equality and finite sets `s` and `t` of type `α`, the cardinality of `s ∪ t` is equal to the cardinality of `s` plus the cardinality of `t` minus the cardinality of `s ∩ t`.
`Multiset.toFinset_card_of_nodup` theorem Multiset.toFinset_card_of_nodup : ∀ {α : Type u_1} [inst : DecidableEq α] {m : Multiset α}, m.Nodup → m.toFinset.card = Multiset.card m The theorem `Multiset.toFinset_card_of_nodup` states that for any type `α` with decidable equality and any multiset `m` of that type, if `m` has no duplicate elements (as ensured by `Multiset.Nodup m`), then the cardinality of the finset resulting from `m` by removing duplicates (achieved by `Multiset.toFinset m`) is equal to the cardinality of `m`. In other words, if a multiset has no duplicates, converting it to a finset does not change its cardinality. More concisely: If `m` is a multiset of type `α` with no duplicate elements, then the cardinality of `Multiset.toFinset m` equals the cardinality of `m`.
`Finset.card_union_le` theorem Finset.card_union_le : ∀ {α : Type u_1} [inst : DecidableEq α] (s t : Finset α), (s ∪ t).card ≤ s.card + t.card This theorem, `Finset.card_union_le`, states that for any type `α` that has decidable equality and for any two finite sets `s` and `t` of type `α`, the cardinality (or size) of the union of `s` and `t` is less than or equal to the sum of the cardinalities of `s` and `t`. In other words, the size of the union of two sets is always less than or equal to the sum of the sizes of the two sets. This is analogous to the principle of inclusion-exclusion in set theory. More concisely: For any type `α` with decidable equality and any finite sets `s` and `t` of type `α`, `Card s.union t <= Card s + Card t`.
`Finset.card_image_le` theorem Finset.card_image_le : ∀ {α : Type u_1} {β : Type u_2} {s : Finset α} {f : α → β} [inst : DecidableEq β], (Finset.image f s).card ≤ s.card The theorem `Finset.card_image_le` states that for any types `α` and `β`, any finite set `s` of type `α`, and any function `f` from `α` to `β` where `β` has decidable equality, the cardinality (or size) of the image of `s` under `f` is less than or equal to the cardinality of `s` itself. This corresponds to the intuitive idea that applying a function to a set cannot result in a larger set, since multiple elements in the original set may map to the same element in the image. More concisely: For any finite type `α`, type `β` with decidable equality, finite set `s` of type `α`, and function `f` from `α` to `β`, the cardinality of `f''s` (image of `s` under `f`) is less than or equal to the cardinality of `s`.
`Finset.card_def` theorem Finset.card_def : ∀ {α : Type u_1} (s : Finset α), s.card = Multiset.card s.val The theorem `Finset.card_def` states that for any given set `s` of arbitrary type `α`, the cardinality of the set `s` (denoted by `s.card`) is equal to the cardinality of the multiset representation of that set (denoted by `Multiset.card s.val`). Here, the cardinality of a set or a multiset refers to the sum of the multiplicities of all its elements. For a set, this is simply the number of elements in that set, whereas for a multiset, this includes the repetitions of elements. More concisely: For any set `s` of type `α`, the cardinality of `s` equals the sum of multiplicities of elements in its multiset representation `s.val`. In other words, `#s = Multiset.card s.val`, where `#s` denotes the cardinality of `s`.
`Finset.exists_smaller_set` theorem Finset.exists_smaller_set : ∀ {α : Type u_1} (A : Finset α), ∀ i ≤ A.card, ∃ B ⊆ A, B.card = i This theorem states that for any given finite set `A` of some type `α`, and for any integer `i` less than or equal to the cardinality of `A`, there exists a subset `B` of `A` such that the cardinality of `B` is `i`. In other words, it is always possible to find a subset of `A` with any smaller size up to and including the size of `A`. More concisely: For any finite type `α` and natural number `i` less than or equal to the cardinality of a finite set `A` of type `α`, there exists a subset `B` of `A` with cardinality `i`.
`Finset.card_le_of_subset` theorem Finset.card_le_of_subset : ∀ {α : Type u_1} {s t : Finset α}, s ⊆ t → s.card ≤ t.card This theorem, `Finset.card_le_of_subset`, states that for any two finite sets `s` and `t` of any type `α`, if set `s` is a subset of set `t` then the cardinality of `s` (i.e., the number of elements in `s`) is less than or equal to the cardinality of `t`. In other words, a subset cannot have more elements than the set it is contained in. More concisely: If `s` is a subset of `t`, then the cardinality of `s` is less than or equal to the cardinality of `t`.
`Finset.card_insert_of_not_mem` theorem Finset.card_insert_of_not_mem : ∀ {α : Type u_1} {s : Finset α} {a : α} [inst : DecidableEq α], a ∉ s → (insert a s).card = s.card + 1 This theorem states that for any type `α` with decidable equality and for any finite set `s` of type `α`, if an element `a` of type `α` is not a member of `s`, then the cardinality (or size) of the result of inserting `a` into `s` is the cardinality of `s` plus one. In mathematical terms, if $a \notin s$ then $\|s \cup \{a\}\| = \|s\| + 1$ where $s$ is a finite set and $a$ is an element not in $s$. More concisely: For any finite type `α` with decidable equality, the cardinality of a finite set `s` of type `α` is strictly increased by one when an element not in `s` is added to it.
`Finset.exists_ne_map_eq_of_card_lt_of_maps_to` theorem Finset.exists_ne_map_eq_of_card_lt_of_maps_to : ∀ {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β}, t.card < s.card → ∀ {f : α → β}, (∀ a ∈ s, f a ∈ t) → ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ f x = f y This theorem, known as the Pigeonhole Principle, states that if you have a set of pigeons `s` and a set of pigeonholes `t` (both represented as finite sets of arbitrary types `α` and `β` respectively), and if the size of `t` is less than the size of `s`, then there exists a function `f` mapping each pigeon `a` in `s` to a pigeonhole in `t` such that there are at least two different pigeons `x` and `y` in `s` that map to the same pigeonhole (i.e., `f x = f y`). More concisely: If `\|s\| > \|t\|`, then there exists a function `f: s -> t` with multiple inputs mapping to the same output.
`Mathlib.Data.Finset.Card._auxLemma.1` theorem Mathlib.Data.Finset.Card._auxLemma.1 : ∀ {α : Type u_1} {s : Finset α}, (s.card = 0) = (s = ∅) This theorem states that for any type `α` and any finite set `s` of that type, the cardinality (or size) of `s` being zero is equivalent to `s` being the empty set. In other words, a finite set has zero elements if and only if it is the empty set. More concisely: For any finite type `α`, the set `s` of type `α` has zero cardinality if and only if it is empty.
`Finset.filter_card_add_filter_neg_card_eq_card` theorem Finset.filter_card_add_filter_neg_card_eq_card : ∀ {α : Type u_1} {s : Finset α} (p : α → Prop) [inst : DecidablePred p] [inst_1 : (x : α) → Decidable ¬p x], (Finset.filter p s).card + (Finset.filter (fun a => ¬p a) s).card = s.card This theorem states that for any given type `α` and a finite set `s` of type `α`, along with a decidable predicate `p`, the sum of the cardinality of the subset of `s` for which `p` holds and the cardinality of the subset of `s` for which `p` does not hold (`¬p`) equals the cardinality of the original set `s`. This is essentially a partition of the finite set `s` based on whether the elements satisfy the predicate `p` or not, asserting that the size of the entire set is the sum of the sizes of the two partitions. More concisely: For any finite type `α` and decidable predicate `p` on `α`, the cardinality of `{x : α \| p x}` plus the cardinality of `{x : α \| ¬p x}` equals the cardinality of `α`.
`Finset.exists_intermediate_set` theorem Finset.exists_intermediate_set : ∀ {α : Type u_1} {A B : Finset α} (i : ℕ), i + B.card ≤ A.card → B ⊆ A → ∃ C, B ⊆ C ∧ C ⊆ A ∧ C.card = i + B.card This theorem states that for any given set `A` and a subset `B` of it, we can always find an intermediate set `C` such that `B` is a subset of `C`, `C` is a subset of `A`, and the cardinality of `C` is `i + B.card` for any given natural number `i`. This cardinality of `C` should not exceed the cardinality of `A`. In other words, we can shrink `A` down to any size `i + B.card` without evicting `B`, provided `i + B.card` doesn't exceed the size of `A`. More concisely: For any set `A` and subset `B`, there exists an intermediate set `C` such that `B` is a subset of `C`, `C` is a subset of `A`, and `C.card = B.card + i` for some natural number `i`, with `C.card` not exceeding `A.card`.
`Finset.card_range` theorem Finset.card_range : ∀ (n : ℕ), (Finset.range n).card = n This theorem states that for any natural number `n`, the cardinality of the set `Finset.range n` (which is the set of natural numbers less than `n`) is equal to `n` itself. In other words, the number of natural numbers less than any given natural number `n` is exactly `n`. More concisely: The cardinality of `Finset.range n` equals `n`.
`Finset.card_eq_zero` theorem Finset.card_eq_zero : ∀ {α : Type u_1} {s : Finset α}, s.card = 0 ↔ s = ∅ The theorem `Finset.card_eq_zero` states that for any type `α` and any finite set `s` of type `α`, the cardinality (or size) of `s` is zero if and only if `s` is the empty set. In other words, a finite set has zero elements if and only if it is an empty set. More concisely: A finite set has zero cards if and only if it is empty.
`Finset.eq_of_subset_of_card_le` theorem Finset.eq_of_subset_of_card_le : ∀ {α : Type u_1} {s t : Finset α}, s ⊆ t → t.card ≤ s.card → s = t This theorem states that for any two finite sets `s` and `t` of any type `α`, if `s` is a subset of `t` and the cardinality of `t` is less than or equal to the cardinality of `s`, then `s` must be equal to `t`. In other words, if a set `s` is completely contained within another set `t`, and `t` has equal or fewer elements than `s`, then the two sets are identical. More concisely: If `s` is a subset of `t` and the cardinality of `s` is greater than or equal to that of `t`, then `s` equals `t`.
`Finset.cast_card_erase_of_mem` theorem Finset.cast_card_erase_of_mem : ∀ {α : Type u_1} {a : α} [inst : DecidableEq α] {R : Type u_4} [inst_1 : AddGroupWithOne R] {s : Finset α}, a ∈ s → ↑(s.erase a).card = ↑s.card - 1 This theorem states that for any type `α` with decidable equality, any element `a` of type `α`, any additive group with one `R`, and any finite set `s` of elements of type `α`, if `a` is an element of `s` then the cardinality of the set `s` with `a` removed is equal to the cardinality of `s` minus one. This result is expressed in the context of an additive group with one, providing a way to avoid having to work with subtraction in the natural numbers. In mathematical notation, this can be written as "#(s \ {a}) = #s - 1" if "a" is an element of "s". More concisely: For any type `α` with decidable equality, if `a` is an element of a finite set `s` in an additive group with one, then the cardinality of `s` without `a` is equal to the cardinality of `s` minus one.
`Finset.card_ne_zero_of_mem` theorem Finset.card_ne_zero_of_mem : ∀ {α : Type u_1} {s : Finset α} {a : α}, a ∈ s → s.card ≠ 0 This theorem asserts that for any type `α`, any finite set `s` of `α`, and any element `a` of `α`, if `a` belongs to `s`, then the cardinality (or size) of `s` is not zero. In other words, if a set contains at least one element, its size is not zero. More concisely: For any finite set `s` of type `α` and any element `a` in `s`, the cardinality of `s` is non-zero if `a` is a member of `s`.
`Finset.card_pos` theorem Finset.card_pos : ∀ {α : Type u_1} {s : Finset α}, 0 < s.card ↔ s.Nonempty This theorem, `Finset.card_pos`, states that for any type `α` and any finite set `s` of that type, the cardinality (number of elements) of `s` is greater than 0 if and only if `s` is nonempty. In other words, a finite set `s` has a positive number of elements only when it has at least one element. More concisely: A finite set is nonempty if and only if it has a positive number of elements.
`Finset.card_map` theorem Finset.card_map : ∀ {α : Type u_1} {β : Type u_2} {s : Finset α} (f : α ↪ β), (Finset.map f s).card = s.card This theorem states that for any given types `α` and `β`, given a finset `s` of type `α` and an embedding function `f` from `α` to `β`, the cardinality (or the number of elements) in the finset obtained by mapping `s` through `f` is the same as the cardinality of `s` itself. This is because `f` is an embedding function, ensuring that there are no duplicates in the resultant finset, hence preserving the number of elements. More concisely: For any finset `s` of type `α` and embedding function `f` from `α` to `β`, the cardinality of `s` equals the cardinality of the image `f''(s)`.
`Finset.card_union_of_disjoint` theorem Finset.card_union_of_disjoint : ∀ {α : Type u_1} {s t : Finset α} [inst : DecidableEq α], Disjoint s t → (s ∪ t).card = s.card + t.card This theorem, `Finset.card_union_of_disjoint`, states that for any given type `α` with decidable equality, any two disjoint finite sets `s` and `t` (where disjointness is defined in terms of the bottom element of a lattice), the cardinality or size of their union equals the sum of their individual cardinalities. This is essentially a formalization of the principle from set theory that the size of the union of two disjoint sets is the sum of their sizes. More concisely: For any type `α` with decidable equality, the cardinality of the union of two disjoint finite sets `s` and `t` equals the sum of their individual cardinalities.
`Finset.le_card_of_inj_on_range` theorem Finset.le_card_of_inj_on_range : ∀ {α : Type u_1} {s : Finset α} {n : ℕ} (f : ℕ → α), (∀ i < n, f i ∈ s) → (∀ i < n, ∀ j < n, f i = f j → i = j) → n ≤ s.card This theorem states that for any finite set `s` of type `α`, a natural number `n`, and a function `f` from natural numbers to `α`, if every number less than `n` is mapped by `f` to an element of `s` and `f` is injective on numbers less than `n` (meaning that if `f` maps two different numbers both less than `n` to the same element of `s`, then those two numbers must actually be the same), then `n` is less than or equal to the cardinality of `s`. In other words, it says that if a function maps a certain number of distinct natural numbers into a set, then the size of that set must be at least as large as that number. More concisely: If `f` is a function from natural numbers to a finite set `α` such that the image of every natural number less than `n` is in `s` and `f` is injective on those numbers, then `n ≤ \|s\|`.
`Mathlib.Data.Finset.Card._auxLemma.16` theorem Mathlib.Data.Finset.Card._auxLemma.16 : ∀ {α : Type u_1} {s : Finset α}, (1 < s.card) = ∃ a b, a ∈ s ∧ b ∈ s ∧ a ≠ b This theorem is stating that for any type `α` and any finite set `s` of that type, the cardinality (or size) of `s` being greater than 1 is equivalent to the existence of two distinct elements `a` and `b` in `s`. In other words, if a finite set has more than one element, then there must be at least two different elements in that set. More concisely: For any finite type `α` and non-empty set `s` of type `α`, the cardinality of `s` being greater than 1 if and only if there exist distinct elements `a` and `b` in `s`.
`Finset.card_filter_le` theorem Finset.card_filter_le : ∀ {α : Type u_1} (s : Finset α) (p : α → Prop) [inst : DecidablePred p], (Finset.filter p s).card ≤ s.card := by sorry This theorem states that for any set `s` of type `α` and a property `p` that elements of `α` can possess, when `p` is a decidable predicate, the cardinality (or size) of the subset of `s` that satisfies `p` is less than or equal to the cardinality of the set `s` itself. In simpler terms, it states that the number of elements in a set that satisfy a certain condition is always less than or equal to the total number of elements in the set. More concisely: For any set `s` of type `α` and decidable predicate `p` on `α`, the cardinality of `{x : s \| p x}` is less than or equal to the cardinality of `s`.
`Finset.card_disjUnion` theorem Finset.card_disjUnion : ∀ {α : Type u_1} (s t : Finset α) (h : Disjoint s t), (s.disjUnion t h).card = s.card + t.card The theorem `Finset.card_disjUnion` states that for any two finite sets `s` and `t` of any type `α`, which are disjoint (meaning that their greatest lower bound is the least element, or the intersection is empty), the cardinality of the disjoint union of `s` and `t` is equal to the sum of the cardinalities of `s` and `t`. In other words, the total number of unique elements in the disjoint union of two sets is the sum of the number of unique elements in each set, when the sets do not share any common elements. More concisely: For disjoint finite sets `s` and `t`, the cardinality of their disjoint union equals the sum of their cardinalities.
`Finset.card_image_of_injective` theorem Finset.card_image_of_injective : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} [inst : DecidableEq β] (s : Finset α), Function.Injective f → (Finset.image f s).card = s.card The theorem `Finset.card_image_of_injective` states that for any types `α` and `β`, any function `f : α → β`, and any finite set `s : Finset α`, if the function `f` is injective (meaning that the same output value can only be produced by the same input value), then the cardinality (or size) of the image of the finite set `s` under the function `f` is equal to the cardinality of the original set `s`. In other words, if a function is injective, it does not change the number of distinct elements when mapping a finite set to another. The context `DecidableEq β` signifies that equality between elements of type `β` is decidable. More concisely: If `f : α → β` is an injective function and `s : Finset α` is a finite set, then `#(map f s) = #s`. (Here, `#` denotes the cardinality or size of a set.)
`Finset.Nonempty.card_pos` theorem Finset.Nonempty.card_pos : ∀ {α : Type u_1} {s : Finset α}, s.Nonempty → 0 < s.card This theorem is an alias of the reverse direction of the `Finset.card_pos` theorem. It states that for any type `α` and a finite set `s` of `α`, if the set `s` is non-empty (`s.Nonempty`), then the cardinality of the set `s` (`s.card`) is greater than zero. In mathematical terms, if a set has at least one element, its size or cardinality is positive. More concisely: If `s` is a finite, non-empty set, then `s.card` is a positive natural number.
`Finset.card_insert_eq_ite` theorem Finset.card_insert_eq_ite : ∀ {α : Type u_1} {s : Finset α} {a : α} [inst : DecidableEq α], (insert a s).card = if a ∈ s then s.card else s.card + 1 The theorem `Finset.card_insert_eq_ite` states that for any type `α` with decidable equality, any finite set `s` of type `α`, and any element `a` of type `α`, the cardinality (or size) of the set obtained by inserting `a` into `s` is equal to the cardinality of `s` itself if `a` is already an element of `s`, otherwise it is equal to the cardinality of `s` plus one. It's a description of how the size of a finite set changes (or doesn't change) when an element is added to it, considering whether the element is already in the set or not. More concisely: For any finite type `α` with decidable equality, the cardinality of a finite set `s` equals the cardinality of `s.insert(a)` if `a` is in `s`, and the cardinality of `s.insert(a)` is one more than the cardinality of `s` otherwise.
`Finset.card_inter_add_card_union` theorem Finset.card_inter_add_card_union : ∀ {α : Type u_1} [inst : DecidableEq α] (s t : Finset α), (s ∩ t).card + (s ∪ t).card = s.card + t.card The theorem `Finset.card_inter_add_card_union` states that for any type `α` with decidable equality and for any two finite sets `s` and `t` of type `α`, the cardinality of the intersection of `s` and `t` added to the cardinality of the union of `s` and `t` is equal to the sum of the cardinalities of `s` and `t`. This is essentially the principle of inclusion-exclusion for two sets, often expressed in set theory as $\|A \cap B\| + \|A \cup B\| = \|A\| + \|B\|$. More concisely: For any type `α` with decidable equality and finite sets `s` and `t` of type `α`, the cardinality of `s ∩ t` plus the cardinality of `s ∪ t` equals the sum of the cardinalities of `s` and `t`.
`Finset.card_le_card_of_inj_on` theorem Finset.card_le_card_of_inj_on : ∀ {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} (f : α → β), (∀ a ∈ s, f a ∈ t) → (∀ a₁ ∈ s, ∀ a₂ ∈ s, f a₁ = f a₂ → a₁ = a₂) → s.card ≤ t.card This theorem states that for any two finite sets `s` and `t` of arbitrary types `α` and `β`, respectively, if a function `f` maps each element of `s` to an element of `t` and `f` is injective (meaning that different elements in `s` map to different elements in `t`), then the cardinality (or size) of `s` is less than or equal to the cardinality of `t`. In other words, an injective function from `s` to `t` cannot increase the size of the set. More concisely: If `f` is an injective function from finite sets `s` and `t` with types `α` and `β` respectively, then the cardinality of `s` is less than or equal to the cardinality of `t`.
`Finset.card_insert_le` theorem Finset.card_insert_le : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α) (s : Finset α), (insert a s).card ≤ s.card + 1 This theorem states that for any type `α` with decidable equality (i.e., for any two elements `a` and `b` of `α`, it's possible to decide whether `a = b` or not), any element `a` of `α`, and any finite set `s` of `α`, the cardinality (size, or number of distinct elements) of the set resulting from inserting `a` into `s` is less than or equal to the cardinality of `s` plus one. This stems from the fact that if `a` is already in `s`, the size of the set does not increase when `a` is inserted; otherwise, it increases by one. More concisely: For any type `α` with decidable equality and any finite set `s` in `α`, the cardinality of `s` and the cardinality of `s.insert(a)` differ by at most 1, where `a` is any element of `α`.
`Finset.card_eq_one` theorem Finset.card_eq_one : ∀ {α : Type u_1} {s : Finset α}, s.card = 1 ↔ ∃ a, s = {a} This theorem states that for any type `α` and any finite set `s` of that type, the cardinality of `s` is equal to one if and only if there exists an element `a` such that `s` is the singleton set containing `a`. In other words, a set has exactly one element if and only if it is the set containing that one element. More concisely: For any type `α` and finite set `s` of type `α`, the set `s` has cardinality one if and only if it is a singleton set.
`Finset.card_sdiff` theorem Finset.card_sdiff : ∀ {α : Type u_1} {s t : Finset α} [inst : DecidableEq α], s ⊆ t → (t \ s).card = t.card - s.card The theorem `Finset.card_sdiff` states that for all types `α`, for all sets `s` and `t` of type `α` where `α` has decidable equality, if `s` is a subset of `t`, then the cardinality (or the number of elements) of the difference of `t` and `s` is equal to the difference of the cardinalities of `t` and `s`. This theorem essentially gives a way to calculate the number of elements in the set difference `t \ s` in terms of the cardinalities of `t` and `s`. More concisely: If `α` has decidable equality and `s` is a subset of `t` in type `α`, then the cardinality of `t \ s` equals the difference of the cardinalities of `t` and `s`.
`Finset.card_mono` theorem Finset.card_mono : ∀ {α : Type u_1}, Monotone Finset.card The theorem `Finset.card_mono` states that for any type `α`, the function `Finset.card` is monotone. This means that if you have two finite sets `a` and `b` of the same type, and `a` is a subset of `b` (in other words `a ≤ b`), then the cardinality of `a` (how many elements `a` contains) is less than or equal to the cardinality of `b` (how many elements `b` contains). This is represented by `Finset.card a ≤ Finset.card b`. More concisely: For any type `α`, the function `Finset.card` on finite sets of type `α` is monotone, i.e., `Finset.card a ≤ Finset.card b` whenever `a ≤ b` are finite sets of type `α`.
`Finset.card_empty` theorem Finset.card_empty : ∀ {α : Type u_1}, ∅.card = 0 This theorem states that for all types `α`, the cardinality (or size) of an empty `Finset` (or finite set) is equal to 0. In other words, there are no elements in an empty set, no matter what the type of the elements is supposed to be. More concisely: The cardinality of an empty finite set is 0.
`Finset.card_image_of_injOn` theorem Finset.card_image_of_injOn : ∀ {α : Type u_1} {β : Type u_2} {s : Finset α} {f : α → β} [inst : DecidableEq β], Set.InjOn f ↑s → (Finset.image f s).card = s.card The theorem `Finset.card_image_of_injOn` states that for any types `α` and `β`, any finite set `s` of type `α`, and any function `f` from `α` to `β` (where `β` has decidable equality), if the function `f` is injective on the set `s` (i.e., no two different elements of `s` map to the same element of `β`), then the cardinality (or size) of the image of `s` under `f` is equal to the cardinality of the set `s`. In other words, when mapping a finite set using an injective function, the number of elements in the output set is the same as the number of elements in the input set. More concisely: If `f: α → β` is a function from a finite set `s ⊆ α` to `β` with decidable equality such that `f` is injective on `s`, then `#s = #(image s f)`.
`Multiset.toFinset_card_le` theorem Multiset.toFinset_card_le : ∀ {α : Type u_1} [inst : DecidableEq α] (m : Multiset α), m.toFinset.card ≤ Multiset.card m The theorem `Multiset.toFinset_card_le` states that for any type `α` that has decidable equality (`DecidableEq α`), and for any multiset `m` of type `α`, the cardinality (or size) of the finset obtained by removing duplicates from `m` (`Multiset.toFinset m`) is less than or equal to the cardinality of `m` itself. In simpler terms, the theorem asserts that when duplicates are removed from a multiset to form a finset, the size of the resulting finset will always be less than or equal to the size of the original multiset. More concisely: For any multiset `m` of type `α` with decidable equality, the cardinality of `Multiset.toFinset m` is less than or equal to the cardinality of `m`.
`Finset.card_erase_of_mem` theorem Finset.card_erase_of_mem : ∀ {α : Type u_1} {s : Finset α} {a : α} [inst : DecidableEq α], a ∈ s → (s.erase a).card = s.card - 1 This theorem states that for any type `α` with decidable equality and for any finite set `s` of type `α` and an element `a` of type `α`, if `a` is an element of `s`, then the cardinality of the set obtained by erasing `a` from `s`, denoted by `Finset.erase s a`, is equal to the cardinality of `s` minus one. In mathematical terms, if $a \in s$, then the number of elements in $s$ without $a$, denoted by $\#(s \setminus \{a\})$, is equal to the number of elements in $s$ minus one, i.e., $\#(s \setminus \{a\}) = \#s - 1$. More concisely: For any finite type `α` with decidable equality, if `a` is an element of a finite set `s` of type `α`, then the cardinality of `s` without `a` equals the cardinality of `s` minus one. (Or, in mathematical notation, if $a \in s$, then $\#(s \setminus \{a\}) = \#s - 1$.)
`Finset.card_doubleton` theorem Finset.card_doubleton : ∀ {α : Type u_1} {a b : α} [inst : DecidableEq α], a ≠ b → {a, b}.card = 2 This theorem, known as `Finset.card_doubleton`, states that for any type `α` with decidable equality, and any two distinct elements `a` and `b` of `α`, the cardinality (number of elements) of the set that contains only `a` and `b` is 2. More concisely: For any type `α` with decidable equality, the cardinality of the finite set `{a, b}` consisting of two distinct elements `a` and `b` of `α` is 2.
`Finset.card_le_one_iff` theorem Finset.card_le_one_iff : ∀ {α : Type u_1} {s : Finset α}, s.card ≤ 1 ↔ ∀ {a b : α}, a ∈ s → b ∈ s → a = b := by sorry This theorem states that for any finite set `s` of a certain type `α`, the cardinality of `s` is less than or equal to one if and only if for any two elements `a` and `b` of type `α`, if `a` and `b` are in `s`, then `a` is equal to `b`. In other words, a set has at most one unique element if any two elements in the set must be the same. More concisely: A finite set `s` of type `α` has at most one element if and only if all distinct elements of `s` are equal.
`Finset.card_pair` theorem Finset.card_pair : ∀ {α : Type u_1} {a b : α} [inst : DecidableEq α], a ≠ b → {a, b}.card = 2 This theorem, named `Finset.card_pair`, establishes that for any given type `α` with decidable equality (i.e., for any two elements `a` and `b` of type `α`, we can determine whether `a = b`), if `a` is not equal to `b`, then the cardinality (size) of the finite set containing `a` and `b` is `2`. In other words, if `a` and `b` are distinct elements of a type that allows for deciding equality, then the set `{a, b}` has exactly two elements. More concisely: For any type `α` with decidable equality, the cardinality of the finite set `{a, b}` is `2` when `a` and `b` are distinct elements of `α`.
`Finset.card_cons` theorem Finset.card_cons : ∀ {α : Type u_1} {s : Finset α} {a : α} (h : a ∉ s), (Finset.cons a s h).card = s.card + 1 The theorem `Finset.card_cons` states that for any type `α`, any finite set `s` of type `α`, and any element `a` of type `α`, if `a` does not belong to `s`, then the cardinality (i.e., the number of elements) of the set formed by adding `a` to `s` (using the `Finset.cons` function) is equal to the cardinality of `s` plus one. In more mathematical terms, if $a \notin s$, then $\| \{a\} \cup s \| = \|s\| + 1$. More concisely: For any type `α` and finite set `s` of type `α`, if `a` is not an element of `s`, then the cardinality of `s ∪ {a}` equals the cardinality of `s` plus one.
`Finset.card_le_one` theorem Finset.card_le_one : ∀ {α : Type u_1} {s : Finset α}, s.card ≤ 1 ↔ ∀ a ∈ s, ∀ b ∈ s, a = b This theorem states that for any finite set `s` of a certain type `α`, the cardinality (or size) of `s` is less than or equal to 1 if and only if for every pair of elements `a` and `b` in `s`, `a` is equal to `b`. In other words, all elements in the set are identical if the set's size is 1 or less. More concisely: For a finite set `s` of type `α`, the cardinality of `s` is equal to 1 if and only if all elements in `s` are equal.
`Finset.card_attach` theorem Finset.card_attach : ∀ {α : Type u_1} {s : Finset α}, s.attach.card = s.card The theorem `Finset.card_attach` asserts that, for any finite set `s` of a certain type `α`, the cardinality (or size) of the set that results from attaching `s` (which consists of the elements of `s` as an element of the subtype `{x // x ∈ s}`), is equal to the cardinality of `s` itself. In other words, attaching a finite set to its elements doesn't change its size. More concisely: For any finite set `s` of type `α`, the cardinality of the set `{x // x ∈ s}` is equal to the cardinality of `s`.
`Finset.card_lt_card` theorem Finset.card_lt_card : ∀ {α : Type u_1} {s t : Finset α}, s ⊂ t → s.card < t.card This theorem states that for any two finite sets `s` and `t` of any type `α`, if `s` is a proper subset of `t` (i.e., `s` is contained within `t` but `s` is not equal to `t`), then the cardinality (or size) of `s` is less than the cardinality of `t`. In other words, a proper subset of a finite set has fewer elements than the set itself. More concisely: For any finite sets `s` and `t` of type `α`, if `s` is a proper subset of `t`, then `#s` (the cardinality of `s`) is strictly less than `#t` (the cardinality of `t`).
`Finset.card_erase_eq_ite` theorem Finset.card_erase_eq_ite : ∀ {α : Type u_1} {s : Finset α} {a : α} [inst : DecidableEq α], (s.erase a).card = if a ∈ s then s.card - 1 else s.card The theorem `Finset.card_erase_eq_ite` states that for any type `α` with decidable equality, any finset `s` of type `α`, and any element `a` of type `α`, the cardinality (size) of the finset obtained by erasing `a` from `s` is equal to the cardinality of `s` minus one if `a` is an element of `s`, and it's equal to the cardinality of `s` otherwise. In other words, if `a` is in `s`, erasing `a` from `s` reduces its cardinality by one, but if `a` is not in `s`, erasing `a` doesn't change the cardinality of `s`. This theorem is also relevant when you already know that `a` is in `s`, as in `Finset.card_erase_of_mem`, or when you know that `a` is not in `s`, as in `Finset.erase_eq_of_not_mem`. More concisely: For any decidably equal type `α` and finset `s` of type `α`, the cardinality of `s` with an element `a` erased is equal to the cardinality of `s` if `a` is not in `s`, and one less if `a` is in `s`.
`Finset.card_singleton` theorem Finset.card_singleton : ∀ {α : Type u_1} (a : α), {a}.card = 1 This theorem states that for any given type `α` and any element `a` of type `α`, the cardinality of the set or "finset" containing only `a` is equal to 1. In other words, the number of elements in a singleton set (a set containing just one element) is always one, regardless of what that element is. More concisely: For any type `α` and any element `a` of type `α`, the cardinality of the singleton set `{a}` is equal to 1.
`Finset.subset_iff_eq_of_card_le` theorem Finset.subset_iff_eq_of_card_le : ∀ {α : Type u_1} {s t : Finset α}, t.card ≤ s.card → (s ⊆ t ↔ s = t) := by sorry This theorem states that for any two finite sets `s` and `t` of any type `α`, if the cardinality (or size) of `t` is less than or equal to the cardinality of `s`, then `s` is a subset of `t` if and only if `s` is equal to `t`. Essentially, it's saying that if a set `t` has the same size or larger compared to another set `s`, the only way for `s` to be a subset of `t` is that they are actually the same set. More concisely: For finite sets `s` and `t` of type `α`, if `\|s\| ≤ \|t\|`, then `s ⊆ t` if and only if `s = t`.
`Finset.card_le_card` theorem Finset.card_le_card : ∀ {α : Type u_1} {s t : Finset α}, s ⊆ t → s.card ≤ t.card This theorem states that for any two finite sets `s` and `t` of any type `α`, if set `s` is a subset of set `t`, then the cardinality (or the number of elements) of set `s` is less than or equal to the cardinality of set `t`. This is a fundamental property of finite sets in set theory. More concisely: For any finite sets `s` and `t` of type `α`, if `s` is a subset of `t`, then `#s ≤ #t`, where `#s` denotes the cardinality of `s`.
`Finset.Nonempty.strong_induction` theorem Finset.Nonempty.strong_induction : ∀ {α : Type u_1} {p : (s : Finset α) → s.Nonempty → Prop}, (∀ (a : α), p {a} ⋯) → (∀ ⦃s : Finset α⦄ (hs : s.Nontrivial), (∀ (t : Finset α) (ht : t.Nonempty), t ⊂ s → p t ht) → p s ⋯) → ∀ ⦃s : Finset α⦄ (hs : s.Nonempty), p s hs The theorem "Finset.Nonempty.strong_induction" states that if we can define a property `p` on a singleton `Finset` and, given any nontrivial `Finset` `s`, we can define `p` on `s` assuming `p` holds for all nonempty strict subsets of `s`, then we can define `p` on any nonempty `Finset`. In other words, it provides a mechanism for strong induction over nonempty finite sets. However, currently, this theorem can only be used to prove properties due to a limitation in `Finset.Nonempty.exists_eq_singleton_or_nontrivial`, which needs computational content to allow `p` to be `Sort`-valued. More concisely: If a property `p` can be defined on singletons and extended to nonempty finite sets using the hypothesis that it holds for all nonempty strict subsets, then `p` can be defined on any nonempty finite set.
`Finset.exists_of_one_lt_card_pi` theorem Finset.exists_of_one_lt_card_pi : ∀ {ι : Type u_4} {α : ι → Type u_5} [inst : (i : ι) → DecidableEq (α i)] {s : Finset ((i : ι) → α i)}, 1 < s.card → ∃ i, 1 < (Finset.image (fun x => x i) s).card ∧ ∀ (ai : α i), Finset.filter (fun x => x i = ai) s ⊂ s The theorem `Finset.exists_of_one_lt_card_pi` states the following: For any finite set `s` of functions from some type `ι` to a family of types `α i` (where `i` ranges over `ι`), if `s` has more than one element, then there exists some `i` such that when we project `s` onto that `i` (i.e., take the image of `s` under the function that returns the `i`-th component), we get a set with more than one element. Moreover, for any element `ai` in the image, the preimage of `ai` under the projection (i.e., the subset of `s` where the `i`-th component equals `ai`) is a proper subset of `s`. In mathematical terms, this means that if we have a nontrivial finite set of functions, then some coordinate is nontrivial and the fibers over every point in this coordinate are nontrivial. More concisely: If `s` is a finite non-empty set of functions from type `ι` to a family of types `α i`, then there exists an `i` such that the preimage of any element in the image of `s` under the `i`-th projection is a proper subset of `s` and has more than one element.
`Finset.one_lt_card` theorem Finset.one_lt_card : ∀ {α : Type u_1} {s : Finset α}, 1 < s.card ↔ ∃ a ∈ s, ∃ b ∈ s, a ≠ b This theorem states that for any finite set `s` of some type `α`, the cardinality of `s` is greater than one if and only if there exist two distinct elements `a` and `b` in `s`. In other words, a set has more than one element if and only if it contains at least two elements that are not the same. More concisely: A finite set `s` of type `α` has cardinality greater than one if and only if there exist distinct elements `a` and `b` in `s`.
`Finset.card_le_one_of_subsingleton` theorem Finset.card_le_one_of_subsingleton : ∀ {α : Type u_1} [inst : Subsingleton α] (s : Finset α), s.card ≤ 1 := by sorry This theorem states that for any given type `α` which is a subsingleton (i.e., it has at most one distinct element), any finite set (`Finset`) of this type `α` can have a cardinality (size) of at most one. Basically, this theorem ensures that if we have a set of a type where all elements are identical, then the size of the set can only be zero or one. More concisely: For any subsingleton type `α`, the cardinality of any finite set of `α` is at most 1.

LeanAide GPT-4 documentation

Module: Mathlib.Data.Finset.Card

Finset.card_union_add_card_inter

theorem Finset.card_union_add_card_inter : ∀ {α : Type u_1} [inst : DecidableEq α] (s t : Finset α), (s ∪ t).card + (s ∩ t).card = s.card + t.card

Multiset.toFinset_card_of_nodup

theorem Multiset.toFinset_card_of_nodup : ∀ {α : Type u_1} [inst : DecidableEq α] {m : Multiset α}, m.Nodup → m.toFinset.card = Multiset.card m

Finset.card_union_le

theorem Finset.card_union_le : ∀ {α : Type u_1} [inst : DecidableEq α] (s t : Finset α), (s ∪ t).card ≤ s.card + t.card

Finset.card_image_le

theorem Finset.card_image_le : ∀ {α : Type u_1} {β : Type u_2} {s : Finset α} {f : α → β} [inst : DecidableEq β], (Finset.image f s).card ≤ s.card

Finset.card_def

theorem Finset.card_def : ∀ {α : Type u_1} (s : Finset α), s.card = Multiset.card s.val

Finset.exists_smaller_set

theorem Finset.exists_smaller_set : ∀ {α : Type u_1} (A : Finset α), ∀ i ≤ A.card, ∃ B ⊆ A, B.card = i

Finset.card_le_of_subset

theorem Finset.card_le_of_subset : ∀ {α : Type u_1} {s t : Finset α}, s ⊆ t → s.card ≤ t.card

Finset.card_insert_of_not_mem

theorem Finset.card_insert_of_not_mem : ∀ {α : Type u_1} {s : Finset α} {a : α} [inst : DecidableEq α], a ∉ s → (insert a s).card = s.card + 1

Finset.exists_ne_map_eq_of_card_lt_of_maps_to

theorem Finset.exists_ne_map_eq_of_card_lt_of_maps_to : ∀ {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β}, t.card < s.card → ∀ {f : α → β}, (∀ a ∈ s, f a ∈ t) → ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ f x = f y

Mathlib.Data.Finset.Card._auxLemma.1

theorem Mathlib.Data.Finset.Card._auxLemma.1 : ∀ {α : Type u_1} {s : Finset α}, (s.card = 0) = (s = ∅)

Finset.filter_card_add_filter_neg_card_eq_card

theorem Finset.filter_card_add_filter_neg_card_eq_card : ∀ {α : Type u_1} {s : Finset α} (p : α → Prop) [inst : DecidablePred p] [inst_1 : (x : α) → Decidable ¬p x], (Finset.filter p s).card + (Finset.filter (fun a => ¬p a) s).card = s.card

Finset.exists_intermediate_set

theorem Finset.exists_intermediate_set : ∀ {α : Type u_1} {A B : Finset α} (i : ℕ), i + B.card ≤ A.card → B ⊆ A → ∃ C, B ⊆ C ∧ C ⊆ A ∧ C.card = i + B.card

Finset.card_range

theorem Finset.card_range : ∀ (n : ℕ), (Finset.range n).card = n

Finset.card_eq_zero

theorem Finset.card_eq_zero : ∀ {α : Type u_1} {s : Finset α}, s.card = 0 ↔ s = ∅

Finset.eq_of_subset_of_card_le

theorem Finset.eq_of_subset_of_card_le : ∀ {α : Type u_1} {s t : Finset α}, s ⊆ t → t.card ≤ s.card → s = t

Finset.cast_card_erase_of_mem

theorem Finset.cast_card_erase_of_mem : ∀ {α : Type u_1} {a : α} [inst : DecidableEq α] {R : Type u_4} [inst_1 : AddGroupWithOne R] {s : Finset α}, a ∈ s → ↑(s.erase a).card = ↑s.card - 1

Finset.card_ne_zero_of_mem

theorem Finset.card_ne_zero_of_mem : ∀ {α : Type u_1} {s : Finset α} {a : α}, a ∈ s → s.card ≠ 0

Finset.card_pos

theorem Finset.card_pos : ∀ {α : Type u_1} {s : Finset α}, 0 < s.card ↔ s.Nonempty

Finset.card_map

theorem Finset.card_map : ∀ {α : Type u_1} {β : Type u_2} {s : Finset α} (f : α ↪ β), (Finset.map f s).card = s.card

Finset.card_union_of_disjoint

theorem Finset.card_union_of_disjoint : ∀ {α : Type u_1} {s t : Finset α} [inst : DecidableEq α], Disjoint s t → (s ∪ t).card = s.card + t.card

Finset.le_card_of_inj_on_range

theorem Finset.le_card_of_inj_on_range : ∀ {α : Type u_1} {s : Finset α} {n : ℕ} (f : ℕ → α), (∀ i < n, f i ∈ s) → (∀ i < n, ∀ j < n, f i = f j → i = j) → n ≤ s.card

Mathlib.Data.Finset.Card._auxLemma.16

theorem Mathlib.Data.Finset.Card._auxLemma.16 : ∀ {α : Type u_1} {s : Finset α}, (1 < s.card) = ∃ a b, a ∈ s ∧ b ∈ s ∧ a ≠ b

Finset.card_filter_le

theorem Finset.card_filter_le : ∀ {α : Type u_1} (s : Finset α) (p : α → Prop) [inst : DecidablePred p], (Finset.filter p s).card ≤ s.card := by sorry

Finset.card_disjUnion

theorem Finset.card_disjUnion : ∀ {α : Type u_1} (s t : Finset α) (h : Disjoint s t), (s.disjUnion t h).card = s.card + t.card

Finset.card_image_of_injective

theorem Finset.card_image_of_injective : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} [inst : DecidableEq β] (s : Finset α), Function.Injective f → (Finset.image f s).card = s.card

Finset.Nonempty.card_pos

theorem Finset.Nonempty.card_pos : ∀ {α : Type u_1} {s : Finset α}, s.Nonempty → 0 < s.card

Finset.card_insert_eq_ite

theorem Finset.card_insert_eq_ite : ∀ {α : Type u_1} {s : Finset α} {a : α} [inst : DecidableEq α], (insert a s).card = if a ∈ s then s.card else s.card + 1

Finset.card_inter_add_card_union

theorem Finset.card_inter_add_card_union : ∀ {α : Type u_1} [inst : DecidableEq α] (s t : Finset α), (s ∩ t).card + (s ∪ t).card = s.card + t.card

Finset.card_le_card_of_inj_on

theorem Finset.card_le_card_of_inj_on : ∀ {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} (f : α → β), (∀ a ∈ s, f a ∈ t) → (∀ a₁ ∈ s, ∀ a₂ ∈ s, f a₁ = f a₂ → a₁ = a₂) → s.card ≤ t.card

Finset.card_insert_le

theorem Finset.card_insert_le : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α) (s : Finset α), (insert a s).card ≤ s.card + 1

Finset.card_eq_one

theorem Finset.card_eq_one : ∀ {α : Type u_1} {s : Finset α}, s.card = 1 ↔ ∃ a, s = {a}

Finset.card_sdiff

theorem Finset.card_sdiff : ∀ {α : Type u_1} {s t : Finset α} [inst : DecidableEq α], s ⊆ t → (t \ s).card = t.card - s.card

Finset.card_mono

theorem Finset.card_mono : ∀ {α : Type u_1}, Monotone Finset.card

Finset.card_empty

theorem Finset.card_empty : ∀ {α : Type u_1}, ∅.card = 0

Finset.card_image_of_injOn

theorem Finset.card_image_of_injOn : ∀ {α : Type u_1} {β : Type u_2} {s : Finset α} {f : α → β} [inst : DecidableEq β], Set.InjOn f ↑s → (Finset.image f s).card = s.card

Multiset.toFinset_card_le

theorem Multiset.toFinset_card_le : ∀ {α : Type u_1} [inst : DecidableEq α] (m : Multiset α), m.toFinset.card ≤ Multiset.card m

Finset.card_erase_of_mem

theorem Finset.card_erase_of_mem : ∀ {α : Type u_1} {s : Finset α} {a : α} [inst : DecidableEq α], a ∈ s → (s.erase a).card = s.card - 1

Finset.card_doubleton

theorem Finset.card_doubleton : ∀ {α : Type u_1} {a b : α} [inst : DecidableEq α], a ≠ b → {a, b}.card = 2

Finset.card_le_one_iff

theorem Finset.card_le_one_iff : ∀ {α : Type u_1} {s : Finset α}, s.card ≤ 1 ↔ ∀ {a b : α}, a ∈ s → b ∈ s → a = b := by sorry

`Finset.card_union_add_card_inter`

`Multiset.toFinset_card_of_nodup`

`Finset.card_union_le`

`Finset.card_image_le`

`Finset.card_def`

`Finset.exists_smaller_set`

`Finset.card_le_of_subset`

`Finset.card_insert_of_not_mem`

`Finset.exists_ne_map_eq_of_card_lt_of_maps_to`

`Mathlib.Data.Finset.Card._auxLemma.1`

`Finset.filter_card_add_filter_neg_card_eq_card`

`Finset.exists_intermediate_set`

`Finset.card_range`

`Finset.card_eq_zero`

`Finset.eq_of_subset_of_card_le`

`Finset.cast_card_erase_of_mem`

`Finset.card_ne_zero_of_mem`

`Finset.card_pos`

`Finset.card_map`

`Finset.card_union_of_disjoint`

`Finset.le_card_of_inj_on_range`

`Mathlib.Data.Finset.Card._auxLemma.16`

`Finset.card_filter_le`

`Finset.card_disjUnion`

`Finset.card_image_of_injective`

`Finset.Nonempty.card_pos`

`Finset.card_insert_eq_ite`

`Finset.card_inter_add_card_union`

`Finset.card_le_card_of_inj_on`

`Finset.card_insert_le`

`Finset.card_eq_one`

`Finset.card_sdiff`

`Finset.card_mono`

`Finset.card_empty`

`Finset.card_image_of_injOn`

`Multiset.toFinset_card_le`

`Finset.card_erase_of_mem`

`Finset.card_doubleton`

`Finset.card_le_one_iff`

`Finset.card_pair`

`Finset.card_cons`

`Finset.card_le_one`

`Finset.card_attach`

`Finset.card_lt_card`

`Finset.card_erase_eq_ite`

`Finset.card_singleton`

`Finset.subset_iff_eq_of_card_le`

`Finset.card_le_card`

`Finset.Nonempty.strong_induction`

`Finset.exists_of_one_lt_card_pi`

`Finset.one_lt_card`

`Finset.card_le_one_of_subsingleton`