Mathlib.Data.Set.Card._auxLemma.33
theorem Mathlib.Data.Set.Card._auxLemma.33 : ∀ {α : Type u_1} {s : Finset α}, (s.card ≤ 1) = ∀ a ∈ s, ∀ b ∈ s, a = b
This theorem states that for any type `α`, any set `s` of type `α`, and any element `a` of type `α`, if `s` is a finite set, then the membership of `a` in the finite set represented by the finite set `s` is equivalent to the membership of `a` in `s`. In other words, an element is in the `Finset` representation of a finite set if and only if it is in the original set.
More concisely: For any type `α`, any finite set `s` of type `α`, and any `α` element `a`, `a` is in the finite set `s` if and only if `a` is in the `Finset` representation of `s`.
|
Set.encard_eq_one
theorem Set.encard_eq_one : ∀ {α : Type u_1} {s : Set α}, s.encard = 1 ↔ ∃ x, s = {x}
The theorem `Set.encard_eq_one` asserts that for any type `α` and any set `s` of type `α`, the cardinality of the set `s` is one if and only if there exists an element `x` such that `s` is the set containing only `x`. In other words, a set `s` has exactly one element if and only if it is the set which consists precisely of this one specific element.
More concisely: A set has exactly one element if and only if it is a singleton set containing any specific element.
|
Set.ncard_insert_of_not_mem
theorem Set.ncard_insert_of_not_mem :
∀ {α : Type u_1} {s : Set α} {a : α}, a ∉ s → autoParam s.Finite _auto✝ → (insert a s).ncard = s.ncard + 1 := by
sorry
This theorem states that for a given set `s` of some type `α` and an element `a` of type `α`, if `a` is not already a member of `s` and `s` is a finite set (this condition is automatically inferred by the Lean prover), then the cardinality (number of elements) of the set obtained by inserting `a` into `s` is equal to the cardinality of `s` plus one. In other words, inserting a new element into a finite set increases its size by one.
More concisely: For a finite set `s` of type `α` and an element `a` not in `s` of type `α`, |s ∪ {a}| = |s| + 1.
|
Set.eq_empty_or_encard_eq_top_or_encard_diff_singleton_lt
theorem Set.eq_empty_or_encard_eq_top_or_encard_diff_singleton_lt :
∀ {α : Type u_1} (s : Set α), s = ∅ ∨ s.encard = ⊤ ∨ ∃ a ∈ s, (s \ {a}).encard < s.encard
The theorem "Set.eq_empty_or_encard_eq_top_or_encard_diff_singleton_lt" states that for any set of any type `α`, the set is either empty, has cardinality equal to infinity, or there exists an element in the set such that if this element is removed, the cardinality of the resulting set is less than the original set's cardinality. This theorem is intended for use in well-founded induction based on the value of `encard`, which represents the cardinality of a set.
More concisely: For any set `α`, the cardinality of `α` is either 0, infinite, or there exists an element `x ∈ α` such that `α \ {x}` has strictly smaller cardinality than `α`.
|
Set.ncard_inter_add_ncard_diff_eq_ncard
theorem Set.ncard_inter_add_ncard_diff_eq_ncard :
∀ {α : Type u_1} (s t : Set α), autoParam s.Finite _auto✝ → (s ∩ t).ncard + (s \ t).ncard = s.ncard
This theorem, labeled `Set.ncard_inter_add_ncard_diff_eq_ncard`, states that for any type `α` and any two sets `s` and `t` of type `α`, under the automatic parameter condition that the set `s` is finite, the sum of the cardinality of the intersection of `s` and `t` and the cardinality of the difference between `s` and `t` (i.e., elements in `s` but not in `t`) is equal to the cardinality of the set `s`. The cardinality is represented as a natural number. In mathematical terms, this can be written as $|s \cap t| + |s \setminus t| = |s|$, where $|.|$ denotes the cardinality of a set.
More concisely: For any finite set `s` of type `α`, the cardinality of `s ∩ t` plus the cardinality of `s \ t` equals the cardinality of `s`, i.e., `|s ∩ t| + |s \ t| = |s|`.
|
Set.Finite.encard_lt_top
theorem Set.Finite.encard_lt_top : ∀ {α : Type u_1} {s : Set α}, s.Finite → s.encard < ⊤
This theorem states that for any set `s` of a certain type `α`, if that set is finite (as defined by the `Set.Finite` function), then the cardinality of the set (as computed by the `Set.encard` function) is strictly less than positive infinity (`⊤`). In other words, the size of any finite set is a finite number.
More concisely: For any finite set `s` of type `α` in Lean, the cardinality of `s` (as computed by `Set.encard`) is a finite natural number less than infinity (`⊤`).
|
Set.Infinite.ncard
theorem Set.Infinite.ncard : ∀ {α : Type u_1} {s : Set α}, s.Infinite → s.ncard = 0
This theorem states that for any type `α` and any set `s` of type `α`, if the set `s` is infinite, then the cardinality of `s` as given by the function `Set.ncard` is equal to `0`. In other words, the cardinality function `Set.ncard` returns the value `0` for any infinite set.
More concisely: For any type `α` and any infinite set `s` of type `α`, the cardinality of `s` as given by `Set.ncard` is equal to 0.
|
Set.ncard_le_of_subset
theorem Set.ncard_le_of_subset :
∀ {α : Type u_1} {s t : Set α}, s ⊆ t → autoParam t.Finite _auto✝ → s.ncard ≤ t.ncard
This theorem, `Set.ncard_le_of_subset`, states that for any two sets `s` and `t` of a type `α`, if `s` is a subset of `t`, and if `t` is finite (where the finiteness of `t` is automatically inferred from the context), then the cardinality of `s` is less than or equal to the cardinality of `t`. Here, the cardinality of a set is denoted by `ncard`, and it refers to the number of elements in the set.
More concisely: For any finite sets `s ⊆ t` of type `α`, the cardinality of `s` is less than or equal to the cardinality of `t`. (In Lean, this theorem is denoted as `Set.ncard_le_of_subset`. )
|
Set.ncard_le_ncard
theorem Set.ncard_le_ncard : ∀ {α : Type u_1} {s t : Set α}, s ⊆ t → autoParam t.Finite _auto✝ → s.ncard ≤ t.ncard := by
sorry
The theorem `Set.ncard_le_ncard` states that for any type `α`, and any two sets `s` and `t` of type `α`, if `s` is a subset of `t`, and `t` is finite (inferred automatically), then the cardinality of `s` (denoted as `Set.ncard s`) is less than or equal to the cardinality of `t` (denoted as `Set.ncard t`). This is a generalization of the intuitive concept that a subset of a finite set cannot have more elements than the set itself.
More concisely: If `α` is a type, `s` and `t` are sets of type `α`, and `s` is a subset of `t` with `t` finite, then `Set.ncard s ≤ Set.ncard t`.
|
Set.encard_singleton
theorem Set.encard_singleton : ∀ {α : Type u_1} (e : α), {e}.encard = 1
This theorem states that for any element `e` of any type `α`, the cardinality of the set containing just that element (`{e}`) is 1. In mathematical terms, if we have a singleton set (a set containing exactly one element), the cardinality of that set is always 1, regardless of what the element is or its type. The function `Set.encard` is used to determine this cardinality.
More concisely: For any type `α` and any element `e` of type `α`, the singleton set `{e}` has cardinality 1.
|
Set.encard_eq_zero
theorem Set.encard_eq_zero : ∀ {α : Type u_1} {s : Set α}, s.encard = 0 ↔ s = ∅
This theorem states that for any set `s` of elements of some type `α`, the cardinality of the set `s` is zero if and only if the set `s` is the empty set. In other words, the only set with a cardinality of zero is the empty set. This is represented in Lean 4 as `Set.encard s = 0 ↔ s = ∅`, where `Set.encard s` denotes the cardinality of set `s` and `∅` represents the empty set.
More concisely: The set `s` hascardinality zero if and only if `s` is the empty set.
|
Set.nonempty_of_encard_ne_zero
theorem Set.nonempty_of_encard_ne_zero : ∀ {α : Type u_1} {s : Set α}, s.encard ≠ 0 → s.Nonempty
This theorem states that for any type `α` and a set `s` of type `α`, if the cardinality (or size) of the set `s` is not zero, then the set `s` is nonempty. In other words, if a set has a non-zero number of elements, it must contain at least one element.
More concisely: If a set is non-empty, then its cardinality is positive.
|
Set.ncard_coe_Finset
theorem Set.ncard_coe_Finset : ∀ {α : Type u_1} (s : Finset α), (↑s).ncard = s.card
This theorem states that for any finite set `s` of type `α`, the cardinality of `s` when it's considered as a general set (by means of the coercion operator `↑s`) equals to the cardinality of `s` as a finite set. In other words, the cardinality operation on a finite set `s`, as performed by `Set.ncard`, gives the same result as the cardinality operation on `s` as a `Finset`, performed by the `.card` function. This theorem bridges the two different views of a finite set, one as a general set and the other as a `Finset` in Lean 4.
More concisely: For any finite set `s` of type `α` in Lean 4, the cardinality of `s` as a general set is equal to the cardinality of `s` considered as a `Finset`.
|
Set.eq_of_subset_of_ncard_le
theorem Set.eq_of_subset_of_ncard_le :
∀ {α : Type u_1} {s t : Set α}, s ⊆ t → t.ncard ≤ s.ncard → autoParam t.Finite _auto✝ → s = t
This theorem states that for any given type `α` and any given sets `s` and `t` of this type, if `s` is a subset of `t` and the cardinality of `t` is less than or equal to the cardinality of `s` (with the assumption that `t` is a finite set), then `s` and `t` are actually the same set. Note that the `autoParam` for `Set.Finite t` is a mechanism to automatically provide the proof for `t` being a finite set.
More concisely: If `α` is a type, `s` and `t` are subsets of `α`, `s` is a subset of `t`, and `t` is finite, then `s` and `t` are equal.
|
Set.InjOn.encard_image
theorem Set.InjOn.encard_image :
∀ {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β}, Set.InjOn f s → (f '' s).encard = s.encard
This theorem states that for any types `α` and `β`, a set `s` of type `α`, and a function `f` from `α` to `β`, if the function `f` is injective on the set `s` (i.e., no two different elements in `s` map to the same element in `β`), then the cardinality (size) of the image of the set `s` under the function `f` equals the cardinality of the set `s`. In other words, an injective function doesn't change the size of the set when mapping it to another set.
More concisely: If `f : α → β` is an injective function and `s : set α`, then the cardinality of `s` equals the cardinality of `{x ∈ s | f x ∈ image f s}`.
|
Set.exists_intermediate_Set
theorem Set.exists_intermediate_Set :
∀ {α : Type u_1} {s t : Set α} (i : ℕ),
i + s.ncard ≤ t.ncard → s ⊆ t → ∃ r, s ⊆ r ∧ r ⊆ t ∧ r.ncard = i + s.ncard
This theorem states that for any given set `t` and its subset `s` of an arbitrary type `α`, along with an integer `i`, if the cardinality of `s` increased by `i` is less than or equal to the cardinality of `t` and `s` is a subset of `t`, then there exists an intermediate set `r` such that `s` is a subset of `r`, `r` is a subset of `t`, and the cardinality of `r` is equal to the cardinality of `s` increased by `i`. Essentially, we can "shrink" `t` to a desired size while maintaining `s` within it.
More concisely: Given a set `t` and its subset `s` of type `α`, and an integer `i` such that the cardinality of `s` + `i` ≤ cardinality of `t`, there exists a subset `r` of `t` with cardinality equal to `s` + `i` and `s` ⊆ `r` ⊆ `t`.
|
Set.ncard_union_eq
theorem Set.ncard_union_eq :
∀ {α : Type u_1} {s t : Set α},
Disjoint s t → autoParam s.Finite _auto✝ → autoParam t.Finite _auto✝¹ → (s ∪ t).ncard = s.ncard + t.ncard
The theorem `Set.ncard_union_eq` states that for any type `α` and any two sets `s` and `t` of this type, if `s` and `t` are disjoint (i.e., their intersection is the bottom or empty set), and both `s` and `t` are finite sets (which is an automatically inferred assumption), then the cardinality of the union of `s` and `t` is equal to the sum of the cardinalities of `s` and `t`. In other words, the size of the union of two disjoint finite sets is the sum of the sizes of the two sets.
More concisely: If two finite sets are disjoint, then the cardinality of their union is the sum of their cardinalities.
|
Set.finite_of_encard_le_coe
theorem Set.finite_of_encard_le_coe : ∀ {α : Type u_1} {s : Set α} {k : ℕ}, s.encard ≤ ↑k → s.Finite
This theorem states that for any type `α`, any set `s` of type `α`, and any natural number `k`, if the cardinality of set `s` is less than or equal to `k`, then the set `s` is finite. Here, the cardinality of a set is defined as a term in `ℕ∞` (the set of natural numbers including infinity), and a set is considered finite if there exists a natural number `n` such that there is an equivalence between the set and the finite set `Fin n`.
More concisely: For any type `α` and set `s` of type `α`, if the cardinality of `s` is less than or equal to some natural number `k`, then `s` is a finite set.
|
Set.encard_insert_of_not_mem
theorem Set.encard_insert_of_not_mem :
∀ {α : Type u_1} {s : Set α} {a : α}, a ∉ s → (insert a s).encard = s.encard + 1
The theorem `Set.encard_insert_of_not_mem` states that for any type `α`, any set `s` of type `α`, and any element `a` of type `α`, if `a` does not belong to `s` (formally, `a ∉ s`), then the cardinality of the set obtained by inserting `a` into `s` is equal to the cardinality of `s` plus one. In other words, adding a new, unique element to a set increases the size of the set by one.
More concisely: For any set `s` and element `a` such that `a` is not in `s`, the cardinality of `s ∪ {a}` equals the cardinality of `s` plus one.
|
Set.encard_empty
theorem Set.encard_empty : ∀ {α : Type u_1}, ∅.encard = 0
This theorem states that for all types `α`, the cardinality of the empty set is equal to 0. In other words, the number of elements in an empty set, irrespective of the type of the elements that could potentially be in the set, is always zero.
More concisely: The theorem asserts that the empty set, regardless of its element type, has cardinality 0.
|
Set.encard_diff_add_encard_of_subset
theorem Set.encard_diff_add_encard_of_subset :
∀ {α : Type u_1} {s t : Set α}, s ⊆ t → (t \ s).encard + s.encard = t.encard
This theorem states that for any two sets `s` and `t` of the same type `α`, if `s` is a subset of `t`, then the cardinality of the difference of `t` and `s` (denoted as `t \ s`), plus the cardinality of `s`, is equal to the cardinality of `t`. In mathematical terms, we can say that for all sets `s` and `t`, if `s` is a subset of `t`, then |`t \ s`| + |`s`| = |`t`|. This is analogous to the principle that the size of a set is equal to the size of a subset plus the size of the complement of the subset within the set.
More concisely: For sets `s` and `t` of the same type with `s` a subset of `t`, the cardinality of `t` equals the cardinality of `t \ s` plus the cardinality of `s`.
|
Set.encard_lt_top_iff
theorem Set.encard_lt_top_iff : ∀ {α : Type u_1} {s : Set α}, s.encard < ⊤ ↔ s.Finite
The theorem `Set.encard_lt_top_iff` states that for any type `α` and a set `s` of type `α`, the cardinality of set `s` is less than infinity if and only if the set `s` is finite. In other words, it establishes an equivalence between a set's cardinality being finite and the set itself being finite. This theorem can be used to check whether a set is finite or not by examining its cardinality.
More concisely: The theorem `Set.encard_lt_top_iff` asserts that a set is finite if and only if its cardinality is less than the cardinality of the type.
|
Set.ncard_eq_toFinset_card
theorem Set.ncard_eq_toFinset_card :
∀ {α : Type u_1} (s : Set α) (hs : autoParam s.Finite _auto✝), s.ncard = (Set.Finite.toFinset hs).card
The theorem `Set.ncard_eq_toFinset_card` states that for all sets `s` of a certain type `α`, given that `s` is finite (which is automatically deduced by the `autoParam` gadget), the cardinality of `s` (given by `Set.ncard s`) equals the cardinality of the corresponding finite set (`(Set.Finite.toFinset hs).card`). In other words, the number of elements in a finite set `s` is the same whether you count them as elements of a set or as elements of the corresponding finite set.
More concisely: For a finite set `s` of type `α` in Lean, `Set.ncard s` equals the cardinality of the corresponding finite set `(Set.Finite.toFinset hs)`.
|
Set.ncard_image_of_injective
theorem Set.ncard_image_of_injective :
∀ {α : Type u_1} {β : Type u_2} {f : α → β} (s : Set α), Function.Injective f → (f '' s).ncard = s.ncard
The theorem `Set.ncard_image_of_injective` states that for any set `s` of type `α` and any function `f` from `α` to `β` that is injective (i.e., it never maps different elements to the same element), the cardinality (number of elements) of the image of the set `s` under the function `f` is equal to the cardinality of the original set `s`. In mathematical notation, if `f: α → β` is an injective function and `s` is a set of elements of type `α`, then the size of the set `f(s)` is equal to the size of the set `s`.
More concisely: The cardinality of an injectively mapped set is equal to the cardinality of the original set.
|
Set.Infinite.encard_eq
theorem Set.Infinite.encard_eq : ∀ {α : Type u_1} {s : Set α}, s.Infinite → s.encard = ⊤
This theorem states that for any type `α` and any set `s` of type `α`, if `s` is infinite, then the cardinality of `s` (i.e., the number of elements in `s`), represented by `Set.encard s`, equals `⊤` (which stands for "infinity" in Lean 4). In essence, the theorem formalizes the intuitive concept that the cardinality of an infinite set is infinity.
More concisely: If a set `s` of type `α` is infinite, then its cardinality equals the greatest cardinal number `⊤`.
|
Mathlib.Data.Set.Card._auxLemma.8
theorem Mathlib.Data.Set.Card._auxLemma.8 : ∀ {α : Type u} {a b : α}, (a ∈ {b}) = (a = b)
This theorem in Lean 4 states that for any type `α` and any elements `a` and `b` of type `α`, the condition "`a` is an element of the singleton set containing `b`" is equivalent to "`a` is equal to `b`". Essentially, it asserts that a value is an element of a singleton set if and only if it is equal to the single element of that set.
More concisely: For any type `α` and any elements `a`, `b` of type `α`, `a` is an element of the singleton set `{b}` if and only if `a` is equal to `b`.
|
Set.finite_of_ncard_ne_zero
theorem Set.finite_of_ncard_ne_zero : ∀ {α : Type u_1} {s : Set α}, s.ncard ≠ 0 → s.Finite
This theorem states that for any type `α` and any set `s` of type `Set α`, if the cardinality of `s` (returned by `Set.ncard s`) is not equal to zero, then the set `s` is finite. In other words, if a set has a nonzero cardinality, it must be a finite set. This is essentially an assertion about the finiteness of sets based on their cardinality in the mathematical logic context.
More concisely: If a set has nonzero cardinality, then it is finite.
|
Set.Finite.eq_of_subset_of_encard_le
theorem Set.Finite.eq_of_subset_of_encard_le :
∀ {α : Type u_1} {s t : Set α}, t.Finite → s ⊆ t → t.encard ≤ s.encard → s = t
This theorem states that for any two sets `s` and `t` of an arbitrary type `α`, if `t` is a finite set and `s` is a subset of `t`, and the cardinality of `t` is less than or equal to the cardinality of `s`, then `s` and `t` must be the same set. In other words, in the context of finite sets, a subset cannot have a cardinality greater than or equal to the set it is contained in unless it is the same set.
More concisely: If `s` is a subset of finite set `t` of type `α` and the cardinality of `s` is greater than or equal to that of `t`, then `s` and `t` are equal.
|
Set.ncard_le_one_of_subsingleton
theorem Set.ncard_le_one_of_subsingleton : ∀ {α : Type u_1} [inst : Subsingleton α] (s : Set α), s.ncard ≤ 1
This theorem expresses that any set, denoted as `s`, of a type `α` that is a subsingleton (meaning that there can be at most one distinct element of that type) has a cardinality (or size) that is less than or equal to one. In other words, if you have a set of a type where all instances are identical, then the number of distinct elements in the set can only be 0 or 1.
More concisely: Any subsingleton set `s` of type `α` has cardinality at most 1.
|
Set.encard_union_eq
theorem Set.encard_union_eq : ∀ {α : Type u_1} {s t : Set α}, Disjoint s t → (s ∪ t).encard = s.encard + t.encard := by
sorry
This theorem states that for any type `α` and any two sets `s` and `t` of this type that are disjoint (i.e., their intersection is empty), the cardinality of the union of `s` and `t` is equal to the sum of the cardinalities of `s` and `t`. Here, the cardinality of a set is represented as a term in `ℕ∞`, which stands for the extended nonnegative integers (including infinity). The disjointness is defined in a general sense for elements of a lattice, but in this context, it refers to the usual notion of disjoint sets.
More concisely: For any type `α` and disjoint sets `s` and `t` of this type, the cardinality of `s ∪ t` equals the sum of the cardinalities of `s` and `t`.
|
Set.Finite.cast_ncard_eq
theorem Set.Finite.cast_ncard_eq : ∀ {α : Type u_1} {s : Set α}, s.Finite → ↑s.ncard = s.encard
This theorem states that, for any type `α` and any set `s` of type `α`, if `s` is finite, then the cardinality of `s` (as a natural number and converted to an extended natural number) is equal to the cardinality of `s` as an extended natural number. In simpler terms, it states that the conversion of the number of elements in a finite set `s` to an extended natural number is equivalent to the direct computation of the number of elements in `s` as an extended natural number.
More concisely: For any finite set `s` of type `α`, the cardinality of `s` as a natural number equals its cardinality as an extended natural number.
|
Set.encard_le_card
theorem Set.encard_le_card : ∀ {α : Type u_1} {s t : Set α}, s ⊆ t → s.encard ≤ t.encard
This theorem states that for any given type `α`, and any two sets `s` and `t` of that type, if `s` is a subset of `t` (`s ⊆ t`), then the cardinality of `s` (`Set.encard s`) is less than or equal to the cardinality of `t` (`Set.encard t`). In mathematical terms, this theorem asserts that the cardinality of a subset is always less than or equal to the cardinality of the set which contains it.
More concisely: For any type `α` and sets `s` and `t` of type `α`, if `s` is a subset of `t`, then `#s ≤ #t`, where `#s` and `#t` denote the cardinalities of `s` and `t`, respectively.
|
Set.encard_mono
theorem Set.encard_mono : ∀ {α : Type u_3}, Monotone Set.encard
The theorem `Set.encard_mono` states that for any type `α`, the function `Set.encard` is monotone. In other words, if we have two sets `A` and `B` of type `α` such that `A` is a subset of `B` (in other words, `A ≤ B`), then the cardinality of `A` is less than or equal to the cardinality of `B` (in other words, `Set.encard A ≤ Set.encard B`). This is consistent with the intuitive understanding that a subset cannot be larger than the set it is contained within.
More concisely: For any type `α` and sets `A` and `B` of type `α` with `A ≤ B`, we have `Set.encard A ≤ Set.encard B`.
|
Set.ncard_empty
theorem Set.ncard_empty : ∀ (α : Type u_3), ∅.ncard = 0
The theorem `Set.ncard_empty` states that for any type `α`, the cardinality of the empty set is zero. In other words, it says that the number of elements in the empty set, regardless of the type of the elements that could potentially be in the set, is always zero. In mathematical terms, if `s` is the empty set, then `|s| = 0`.
More concisely: For any type `α`, the cardinality of the empty set is 0. (In mathematical notation: |∅| = 0)
|
Set.ncard_def
theorem Set.ncard_def : ∀ {α : Type u_1} (s : Set α), s.ncard = ENat.toNat s.encard
This theorem states that for any set `s` of type `α`, the cardinality of `s` -- denoted as `Set.ncard s` -- is equal to the conversion of `Set.encard s` from `ℕ∞` (extended natural number, which includes infinity) to a natural number `ℕ` using the `ENat.toNat` function. The `ENat.toNat` function converts any `ℕ∞` value to a `ℕ` value, sending infinity (`∞`) to zero (`0`). In other words, if a set is infinite, its cardinality as determined by `Set.ncard` is assigned the value zero.
More concisely: For any set `s` of type `α`, the cardinality `Set.ncard s` is the natural number representation of the infinite cardinality `Set.encard s` obtained by applying `ENat.toNat`. If `s` is infinite, then `Set.ncard s` equals zero.
|
Set.Finite.encard_eq_coe_toFinset_card
theorem Set.Finite.encard_eq_coe_toFinset_card :
∀ {α : Type u_1} {s : Set α} (h : s.Finite), s.encard = ↑h.toFinset.card
This theorem states that for any finite set `s` of a certain type `α`, the cardinality of `s` (when represented as a term in `ℕ∞` using `Set.encard`) is equal to the cardinality of the `Finset` representation of `s` (obtained using `Set.Finite.toFinset`). Here, `card` is used to find the cardinality of the `Finset`, and the `↑` operator is used to coerce this natural number to a term in `ℕ∞`. In other words, the theorem ensures that the notion of the size of a finite set is consistent whether we consider the set as a mathematical set or as a finite set in Lean.
More concisely: For any finite set `s` of type `α`, the cardinality of `s` as represented in `ℕ∞` by `Set.encard` equals the cardinality of the `Finset` representation of `s` obtained using `Set.Finite.toFinset`.
|
Set.encard_diff_add_encard_inter
theorem Set.encard_diff_add_encard_inter : ∀ {α : Type u_1} (s t : Set α), (s \ t).encard + (s ∩ t).encard = s.encard
This theorem states that for any type `α` and any two sets `s` and `t` of type `α`, the cardinality of the difference set `s \ t` added to the cardinality of the intersection set `s ∩ t` is equal to the cardinality of the set `s`. This mirrors the principle of inclusion-exclusion in set theory, with the cardinality functioning analogously to the measure of the set. The difference set `s \ t` contains all elements of `s` that are not in `t`, while the intersection `s ∩ t` includes all elements that `s` and `t` have in common.
More concisely: The cardinality of a set `α` equals the cardinality of its subset `s` plus the cardinality of its complement in `s` relative to the subset `t` minus the cardinality of their intersection, i.e., `|s| = |s ∩ t| + |s \ t|`.
|
Set.exists_smaller_set
theorem Set.exists_smaller_set : ∀ {α : Type u_1} (s : Set α), ∀ i ≤ s.ncard, ∃ t ⊆ s, t.ncard = i
This theorem states that for any set `s` of an arbitrary type `α`, and for any integer `i` less than or equal to the cardinality (number of elements) of `s`, there exists a subset `t` of `s` such that the cardinality of `t` is equal to `i`. In other words, we can always find a smaller or equal sized subset `t` from a given set `s`, where the size of the subset is specified by `i`.
More concisely: For any set `s` and integer `i` less than or equal to its cardinality, there exists a subset `t` of `s` with cardinality `i`.
|
Set.encard_diff_singleton_add_one
theorem Set.encard_diff_singleton_add_one :
∀ {α : Type u_1} {s : Set α} {a : α}, a ∈ s → (s \ {a}).encard + 1 = s.encard
This theorem states that for any type `α`, any set `s` of that type, and any element `a` of that type, if `a` is a member of `s`, then the cardinality of the set obtained by removing `a` from `s` plus one is equal to the cardinality of `s`. In other words, if you have a set and remove a single element, the size of the new set is one less than the original set. This is formalizing in Lean what we intuitively understand about counting elements in a set.
More concisely: For any type `α` and set `s:` `α`, if `a ∈ s`, then the cardinality of `s \ {a}` equals the cardinality of `s`.
|