LeanAide documentation

LeanAide GPT-4 documentation

Module: Mathlib.Data.Set.Basic

`Set.mem_insert_iff` theorem Set.mem_insert_iff : ∀ {α : Type u} {x a : α} {s : Set α}, x ∈ insert a s ↔ x = a ∨ x ∈ s This theorem, `Set.mem_insert_iff`, states that for any type `α` and any elements `x` and `a` of type `α`, and any set `s` of type `α`, the proposition `x` is in the set formed by inserting `a` into `s` if and only if `x` is equal to `a` or `x` is in `s`. In other words, it explains the condition for an element to be in a set to which a new element has been added. More concisely: For any set `s` of type `α` and any `x, a` in `α`, `x ∈ insert a s` if and only if `x = a` or `x ∈ s`.
`Set.not_subset` theorem Set.not_subset : ∀ {α : Type u} {s t : Set α}, ¬s ⊆ t ↔ ∃ a ∈ s, a ∉ t The theorem `Set.not_subset` states that for all types `α` and for all sets `s` and `t` of type `α`, the proposition that `s` is not a subset of `t` is equivalent to the existence of an element `a` in `s` such that `a` is not in `t`. In other words, a set `s` is not a subset of another set `t` if and only if there is at least one element in `s` which does not belong to `t`. More concisely: A set `s` is not a subset of `t` if and only if there exists an element `a` in `s` such that `a` is not in `t`.
`Set.mem_union` theorem Set.mem_union : ∀ {α : Type u} (x : α) (a b : Set α), x ∈ a ∪ b ↔ x ∈ a ∨ x ∈ b The theorem `Set.mem_union` states that for any type `α`, an element `x` of type `α`, and two sets `a` and `b` of type `α`, `x` is a member of the union of `a` and `b` if and only if `x` is a member of `a` or `x` is a member of `b`. This corresponds to the standard mathematical definition of union of sets: an element belongs to the union of two sets if it belongs to at least one of the sets. More concisely: For any type `α` and sets `a` and `b` of type `α`, `x ∈ a ∪ b` if and only if `x ∈ a` or `x ∈ b`.
`Subsingleton.mem_iff_nonempty` theorem Subsingleton.mem_iff_nonempty : ∀ {α : Type u_2} [inst : Subsingleton α] {s : Set α} {x : α}, x ∈ s ↔ s.Nonempty This theorem states that for any type `α` that is a subsingleton (i.e., a type with at most one element), any set `s` of elements of type `α`, and any element `x` of type `α`, `x` is a member of `s` if and only if `s` is nonempty. Essentially, it's saying that, in the context of a subsingleton, the membership of any element in a set is equivalent to the set being nonempty. More concisely: For any subsingleton type `α`, a set `s` of type `α` has exactly one element if and only if `s` is nonempty and contains that element.
`Set.empty_diff` theorem Set.empty_diff : ∀ {α : Type u} (s : Set α), ∅ \ s = ∅ The theorem `Set.empty_diff` states that for all types `α` and for any set `s` of type `α`, the difference between the empty set and `s` is the empty set. In mathematical terms, this is equivalent to saying that the set difference between the empty set (∅) and any set `s` is always the empty set (∅). The `\` symbol represents the set difference operation. More concisely: For all types α and sets s of α, the set difference between the empty set and s is the empty set. (In mathematical notation: ∅ \ s = ∅)
`Set.inter_eq_self_of_subset_right` theorem Set.inter_eq_self_of_subset_right : ∀ {α : Type u} {s t : Set α}, t ⊆ s → s ∩ t = t This theorem states that for any type `α` and any two sets `s` and `t` of this type, if `t` is a subset of `s` (written as `t ⊆ s`), then the intersection of `s` and `t` is equal to `t`. This means that when `t` is a subset of `s`, all elements of `t` are also elements of `s` and thus, all elements that are in both `s` and `t` are precisely the elements of `t`. More concisely: For any type `α` and sets `s` and `t` of this type, if `t` is a subset of `s` (`t ⊆ s`), then `s ∩ t = t`.
`Set.not_mem_compl_iff` theorem Set.not_mem_compl_iff : ∀ {α : Type u} {s : Set α} {x : α}, x ∉ sᶜ ↔ x ∈ s This theorem states that for any set `s` of elements of some type `α` and any element `x` of this type, `x` is not a member of the complement of `s` if and only if `x` is a member of `s`. In other words, an element is not in the complement of a set exactly when it is in the set itself. This is a basic property of complements in set theory. More concisely: The complement of a set is identical to its complement in the sense that an element is in the complement of a set if and only if it is not in the set.
`Set.diff_union_self` theorem Set.diff_union_self : ∀ {α : Type u} {s t : Set α}, s \ t ∪ t = s ∪ t This theorem states that for any type `α`, and any two sets `s` and `t` of type `α`, the union of the set difference `s \ t` (elements in `s` but not in `t`) and `t` is equal to the union of `s` and `t`. Essentially, it means that taking away elements from `s` which are in `t` and then uniting it back with `t` does not change the original union of `s` and `t`. This theorem is a basic result in set theory. More concisely: For any type `α` and sets `s` and `t` of type `α`, `(s \ t) ∪ t = s ∪ t`.
`Set.nonempty_of_mem` theorem Set.nonempty_of_mem : ∀ {α : Type u} {s : Set α} {x : α}, x ∈ s → s.Nonempty This theorem, `Set.nonempty_of_mem`, asserts that for any type `α`, any set `s` of type `α`, and any element `x` of type `α`, if `x` is an element of the set `s` (denoted by `x ∈ s`), then `s` is nonempty. In other words, if a set contains at least one element, then it is not an empty set. The theorem uses the `Set.Nonempty` property which is defined as the existence of at least one element in a set. More concisely: If a set is nonempty and contains an element `x`, then `x` belongs to the set. (Equivalently, if an element `x` belongs to a nonempty set `s`, then `s` is nonempty.)
`Set.ssubset_singleton_iff` theorem Set.ssubset_singleton_iff : ∀ {α : Type u} {s : Set α} {x : α}, s ⊂ {x} ↔ s = ∅ The theorem `Set.ssubset_singleton_iff` states that for any type `α`, any set `s` of type `α`, and any element `x` of type `α`, the set `s` is a strict subset of the singleton set `{x}` if and only if `s` is the empty set. In other words, a set `s` is strictly contained within a singleton set only if `s` is empty. More concisely: For any type `α` and set `s` of type `α`, `s` is a strict subset of the singleton set `{x}` if and only if `s` is empty.
`Set.empty_union` theorem Set.empty_union : ∀ {α : Type u} (a : Set α), ∅ ∪ a = a This theorem states that for any set `a` of some type `α`, the union of the empty set (`∅`) with `a` is equal to `a`. In other words, the operation of taking the union of any set with the empty set leaves the original set unchanged. This is a fundamental property of the union operation in set theory. More concisely: The empty set is a neutral element for set union, i.e., ∅ ∪ A = A for any set A.
`Set.mem_empty_iff_false` theorem Set.mem_empty_iff_false : ∀ {α : Type u} (x : α), x ∈ ∅ ↔ False This theorem states that for any type `α` and any element `x` of this type, the proposition "element `x` belongs to the empty set" is logically equivalent to `False`. In other words, no element can belong to the empty set in the universe of set theory. More concisely: For any type `α` and any of its elements `x`, `x ∈ ∅` is logically equivalent to `False`. (In the context of Lean or set theory, `∅` represents the empty set.)
`Set.mem_of_subset_of_mem` theorem Set.mem_of_subset_of_mem : ∀ {α : Type u} {s₁ s₂ : Set α} {a : α}, s₁ ⊆ s₂ → a ∈ s₁ → a ∈ s₂ This theorem states that for any type `α` and any two sets `s₁` and `s₂` of type `α`, along with any element `a` of type `α`, if `s₁` is a subset of `s₂`, and if `a` is an element of `s₁`, then `a` is also an element of `s₂`. This is essentially the property of subset, stating that all elements of a subset must also be elements of the set that contains it. More concisely: If `s₁` is a subset of `s₂` and `a` is an element of `s₁`, then `a` is an element of `s₂`.
`Set.compl_eq_univ_diff` theorem Set.compl_eq_univ_diff : ∀ {α : Type u} (s : Set α), sᶜ = Set.univ \ s The theorem `Set.compl_eq_univ_diff` states that for any set `s` of a certain type `α`, the complement of `s` (denoted `sᶜ`) is equal to the difference between the universal set of type `α` and `s`. In other words, the complement of a set `s` includes all elements belonging to the universal set that are not in `s`. More concisely: The complement of a set `s` in type `α` is equal to the universal set of `α` minus `s`.
`Set.disjoint_sdiff_inter` theorem Set.disjoint_sdiff_inter : ∀ {α : Type u} {s t : Set α}, Disjoint (s \ t) (s ∩ t) The theorem `Set.disjoint_sdiff_inter` states that for any type `α` and any two sets `s` and `t` of this type, the set difference of `s` and `t` (denoted as `s \ t` in Lean 4) and the intersection of `s` and `t` (denoted as `s ∩ t` in Lean 4) are disjoint. In the context of this theorem, two sets are said to be disjoint if their infimum, or greatest lower bound, is the bottom element of the lattice in which the sets reside. More concisely: For any type `α` and sets `s` and `t` of type `Set α`, the set differences `s \ t` and `t \ s` are disjoint, i.e., their intersection is the empty set.
`Set.union_inter_distrib_right` theorem Set.union_inter_distrib_right : ∀ {α : Type u} (s t u : Set α), (s ∪ t) ∩ u = s ∩ u ∪ t ∩ u This theorem states that for any type `α` and any three sets `s`, `t`, and `u` of this type, the union of `s` and `t` intersected with `u` is equal to the union of the intersection of `s` with `u` and the intersection of `t` with `u`. In mathematical notation, this is represented as $(s \cup t) \cap u = (s \cap u) \cup (t \cap u)$. This theorem essentially demonstrates the distributive property of intersection over union in the context of sets. More concisely: The theorem asserts that for any sets `s`, `t`, and `u`, the intersection of their union and `u` equals the union of their intersections with `u`. In mathematical notation, $(s \cup t) \cap u = (s \cap u) \cup (t \cap u)$.
`Set.insert_comm` theorem Set.insert_comm : ∀ {α : Type u} (a b : α) (s : Set α), insert a (insert b s) = insert b (insert a s) := by sorry This theorem states that for any type 'α', and any elements 'a' and 'b' of this type, as well as any set 's' of this type, the operation of inserting 'a' into the set obtained by inserting 'b' into 's' is equivalent to the operation of inserting 'b' into the set obtained by inserting 'a' into 's'. In other words, the order of insertion does not matter, which is a property of commutativity. More concisely: For any set 's' and elements 'a' and 'b' of type 'α', the operation of inserting 'a' into the set obtained by inserting 'b' into 's' is equal to the operation of inserting 'b' into the set obtained by inserting 'a' into 's'.
`Set.singleton_subset_iff` theorem Set.singleton_subset_iff : ∀ {α : Type u} {a : α} {s : Set α}, {a} ⊆ s ↔ a ∈ s The theorem `Set.singleton_subset_iff` is a statement about sets in a general type `α`. It states that for any element `a` of type `α` and any set `s` of type `α`, the singleton set containing only `a` is a subset of `s` if and only if `a` is an element of `s`. In other words, all the elements of the singleton set `{a}` (which is just `a` itself) are in `s` exactly when `a` is in `s`. This theorem provides a way to relate the subset relation and the membership relation for singleton sets. More concisely: A set {a} is a subset of set s if and only if a is an element of s.
`Subsingleton.eq_univ_of_nonempty` theorem Subsingleton.eq_univ_of_nonempty : ∀ {α : Type u_1} [inst : Subsingleton α] {s : Set α}, s.Nonempty → s = Set.univ The theorem `Subsingleton.eq_univ_of_nonempty` states that for any type `α` that has the `Subsingleton` property (meaning that there can be at most one element of that type), any nonempty set `s` of that type must be equivalent to the universal set on `α`. In other words, if a type can have at most one element and we have a set of that type which contains at least one element, then this set must contain every element of the type, which means that it is equal to the universal set on `α`. More concisely: If `α` is a type with at most one element and `s : set α` is nonempty, then `s` equals the universal set on `α`.
`Set.inter_subset_inter` theorem Set.inter_subset_inter : ∀ {α : Type u} {s₁ s₂ t₁ t₂ : Set α}, s₁ ⊆ t₁ → s₂ ⊆ t₂ → s₁ ∩ s₂ ⊆ t₁ ∩ t₂ This theorem states that for any type `α` and for any four sets `s₁`, `s₂`, `t₁`, `t₂` of type `α`, if set `s₁` is a subset of `t₁` and set `s₂` is a subset of `t₂`, then the intersection of `s₁` and `s₂` is a subset of the intersection of `t₁` and `t₂`. In other words, the intersection of subsets results in a subset of the intersection of their respective superset. More concisely: If `s₁ ⊆ t₁` and `s₂ ⊆ t₂`, then `s₁ ∩ s₂ ⊆ t₁ ∩ t₂`.
`Set.inter_union_distrib_left` theorem Set.inter_union_distrib_left : ∀ {α : Type u} (s t u : Set α), s ∩ (t ∪ u) = s ∩ t ∪ s ∩ u The theorem `Set.inter_union_distrib_left` states that for any type `α` and for any three sets `s`, `t`, and `u` of type `α`, the intersection of `s` with the union of `t` and `u` is the same as the union of the intersection of `s` with `t` and the intersection of `s` with `u`. In mathematical notation, this can be written as $s \cap (t \cup u) = (s \cap t) \cup (s \cap u)$. This is a statement of the distributive property of intersection over union in set theory. More concisely: The theorem `Set.inter_union_distrib_left` asserts that for any sets `s`, `t`, and `u`, $s \cap (t \cup u) = (s \cap t) \cup (s \cap u)$.
`Set.inter_right_comm` theorem Set.inter_right_comm : ∀ {α : Type u} (s₁ s₂ s₃ : Set α), s₁ ∩ s₂ ∩ s₃ = s₁ ∩ s₃ ∩ s₂ This theorem, named `Set.inter_right_comm`, states that for any type `α` and for any three sets `s₁`, `s₂`, and `s₃` of this type, the intersection of `s₁` with the intersection of `s₂` and `s₃` is equal to the intersection of `s₁` with the intersection of `s₃` and `s₂`. In other words, the order in which we take the intersection of `s₂` and `s₃` does not affect the final result; this property is referred to as the right-commutativity of intersection on sets. More concisely: For any type `α` and sets `s₁`, `s₂`, and `s₃` of type `α`, `s₁ ∩ (s₂ ∩ s₃) = s₁ ∩ (s₃ ∩ s₂)`.
`Set.eq_univ_of_univ_subset` theorem Set.eq_univ_of_univ_subset : ∀ {α : Type u} {s : Set α}, Set.univ ⊆ s → s = Set.univ This theorem, `Set.eq_univ_of_univ_subset`, is also known as an alias of the forward direction of `Set.univ_subset_iff`. It states that for any type `α` and any set `s` of type `α`, if the universal set (which contains all elements of type `α`) is a subset of `s`, then `s` is also a universal set. Essentially, if `s` contains all possible elements of `α`, it becomes identical to the universal set. More concisely: If a set `s` contains all elements of type `α`, then `s` is equal to the universal set of type `α`.
`Set.inter_compl_nonempty_iff` theorem Set.inter_compl_nonempty_iff : ∀ {α : Type u} {s t : Set α}, (s ∩ tᶜ).Nonempty ↔ ¬s ⊆ t The theorem `Set.inter_compl_nonempty_iff` states that for any type `α` and for any sets `s` and `t` of type `α`, the set `s` has a non-empty intersection with the complement of `t` if and only if `s` is not a subset of `t`. In other words, there exists at least one element in set `s` that is not in set `t` if and only if `s` is not entirely contained within `t`. More concisely: For sets $s$ and $t$ of type $\alpha$, $s$ has a non-empty intersection with the complement of $t$ if and only if $s$ is not a subset of $t$.
`Set.insert_subset_iff` theorem Set.insert_subset_iff : ∀ {α : Type u} {a : α} {s t : Set α}, insert a s ⊆ t ↔ a ∈ t ∧ s ⊆ t The theorem `Set.insert_subset_iff` asserts that for all types `α`, all elements `a` of type `α`, and all sets `s` and `t` of type `α`, the set resulting from the insertion of `a` into `s` is a subset of `t` if and only if `a` is an element of `t` and `s` is a subset of `t`. In other words, adding an element to a set preserves the subset relation if and only if the added element is also contained in the larger set. More concisely: For all types α, sets s and t of α, and element a of α, the set {a} ∪ s is a subset of t if and only if a ∈ t and s ⊆ t.
`Set.mem_insert` theorem Set.mem_insert : ∀ {α : Type u} (x : α) (s : Set α), x ∈ insert x s This theorem states that for any type `α`, any element `x` of that type, and any set `s` of elements of type `α`, the element `x` belongs to the set that is the result of inserting `x` into `s`. In short, it's confirming the intuitive property that an element is a member of the set that it has been added to. More concisely: For any type `α`, any set `s` of elements from `α`, and any `x` in `α`, `x` belongs to the set `s.insert x`.
`Set.diff_union_of_subset` theorem Set.diff_union_of_subset : ∀ {α : Type u} {s t : Set α}, t ⊆ s → s \ t ∪ t = s The theorem `Set.diff_union_of_subset` states that for any type `α` and for any two sets `s` and `t` of type `α`, if `t` is a subset of `s` then the union of the set difference `s \ t` and the set `t` equals the set `s` itself. In mathematical notation, this would be rendered as if `t ⊆ s` then `(s \ t) ∪ t = s`. More concisely: If `s` contains `t` (i.e., `t ⊆ s`), then `(s \ t) ∪ t = s`.
`Set.diff_subset_iff` theorem Set.diff_subset_iff : ∀ {α : Type u} {s t u : Set α}, s \ t ⊆ u ↔ s ⊆ t ∪ u This theorem, `Set.diff_subset_iff`, states that for all types `α` and for all sets `s`, `t`, and `u` of type `α`, the set difference `s \ t` is a subset of `u` if and only if `s` is a subset of the union of `t` and `u`. In other words, all elements of `s` that are not in `t` belong to `u` if and only if all elements of `s` belong to either `t`, `u`, or both. This theorem is a fundamental result in set theory and forms an essential part of the lattice structure on the power set of a given set. More concisely: For sets `s`, `t`, and `u` in type `α`, `s \ t` is a subset of `u` if and only if `s` is a subset of `t ∪ u`.
`Set.subset_empty_iff` theorem Set.subset_empty_iff : ∀ {α : Type u} {s : Set α}, s ⊆ ∅ ↔ s = ∅ This theorem states that for any type `α` and any set `s` of type `α`, `s` is a subset of the empty set if and only if `s` is the empty set itself. Here, ⊆ denotes the subset relation, meaning every element of `s` is also an element of the empty set. The ⊆ ∅ condition can only be satisfied if `s` is the empty set (∅), as the empty set contains no elements. More concisely: A set `s` is a subset of the empty set if and only if `s` is the empty set.
`Set.union_assoc` theorem Set.union_assoc : ∀ {α : Type u} (a b c : Set α), a ∪ b ∪ c = a ∪ (b ∪ c) The theorem `Set.union_assoc` states that for any type `α` and any three sets `a`, `b`, and `c` of type `α`, the union operation on sets is associative. In other words, taking the union of `a` with the union of `b` and `c` (`a ∪ (b ∪ c)`) is the same as taking the union of the union of `a` and `b` with `c` (`(a ∪ b) ∪ c`). This mirrors the associative property in algebra where the way in which operations are grouped does not change the result of the operation. More concisely: For any type `α` and sets `a`, `b`, and `c` of type `α`, the association of set union operations holds: `(a ∪ b) ∪ c` = `a ∪ (b ∪ c)`.
`Set.inter_subset_inter_right` theorem Set.inter_subset_inter_right : ∀ {α : Type u} {s t : Set α} (u : Set α), s ⊆ t → u ∩ s ⊆ u ∩ t The theorem `Set.inter_subset_inter_right` states that for all types `α`, and for any sets `s`, `t`, and `u` of type `α`, if set `s` is a subset of set `t`, then the intersection of set `u` and set `s` is a subset of the intersection of set `u` and set `t`. In terms of set theory, this means that if we have a set that intersects both `s` and `t`, and `s` is entirely contained within `t`, then the intersection with `s` is also entirely contained within the intersection with `t`. More concisely: If `s` is a subset of `t`, then `s ∩ u` is a subset of `t ∩ u`.
`Set.union_eq_self_of_subset_left` theorem Set.union_eq_self_of_subset_left : ∀ {α : Type u} {s t : Set α}, s ⊆ t → s ∪ t = t This theorem states that for all types `α`, and for all sets `s` and `t` of type `α`, if `s` is a subset of `t` then the union of `s` and `t` is equal to `t`. In more mathematical terms, given two sets `s` and `t`, if every element in `s` is also an element in `t` (i.e., `s ⊆ t`), then the union of `s` and `t` (i.e., `s ∪ t`) is simply `t`. This aligns with the intuition that adding a subset to a set does not change the original set. More concisely: For all types `α` and sets `s` and `t` of type `α`, if `s` is a subset of `t`, then `s ∪ t = t`.
`Membership.mem.out` theorem Membership.mem.out : ∀ {α : Type u} {p : α → Prop} {a : α}, a ∈ {x \| p x} → p a This theorem states that if `a` is an element of a set of elements `x` for which a condition `p` holds, then the condition `p` holds for `a`. In other words, if `a` belongs to the set `{x \| p x}`, then `p a` is true. Despite these being definitionally equal, the theorem can be useful in various ways, for example, to apply further projection notation or in an argument to `simp`. More concisely: If a set contains an element x such that p(x) holds, then p(a) holds for any a in that set.
`Set.Nonempty.mono` theorem Set.Nonempty.mono : ∀ {α : Type u} {s t : Set α}, s ⊆ t → s.Nonempty → t.Nonempty The theorem `Set.Nonempty.mono` states that for any type `α` and any two sets `s` and `t` of this type, if `s` is a subset of `t`, then the non-emptiness of `s` implies the non-emptiness of `t`. In other words, if a set `s` has at least one element and all elements of `s` are also in `t`, then `t` must also have at least one element. More concisely: If `s` is a subset of `t` and `s` is non-empty, then `t` is non-empty.
`Set.disjoint_sdiff_left` theorem Set.disjoint_sdiff_left : ∀ {α : Type u} {s t : Set α}, Disjoint (t \ s) s The theorem `Set.disjoint_sdiff_left` states that for any type `α` and any two sets `s` and `t` of type `α`, the set difference `t \ s` is disjoint from set `s`. In other words, there is no element in `t` that is not in `s` which also belongs to `s`. This is defined in the context of a lattice, where the infimum of the two sets is considered to be the bottom element, symbolized by `⊥`. More concisely: For any type `α` and sets `s` and `t` of type `α`, the set difference `t \ s` is a subset of the complement of `s`. In other words, `t \ s` and `s` have no elements in common.
`Set.mem_setOf` theorem Set.mem_setOf : ∀ {α : Type u} {a : α} {p : α → Prop}, a ∈ {x \| p x} ↔ p a This theorem, `Set.mem_setOf`, relates membership in a set to satisfaction of a property. Specifically, for any type `α`, any element `a` of that type, and any property `p` that applies to elements of type `α`, `a` belongs to the set of elements `x` for which `p x` holds if and only if `p a` holds. In other words, an element `a` is a member of the set described by the property `p` precisely when `a` satisfies the property `p`. More concisely: For any type `α`, set `S` defined as `{x : α \| p x}`, and element `a` of type `α`, `a` is a member of `S` if and only if `p a` holds.
`Set.inter_union_diff` theorem Set.inter_union_diff : ∀ {α : Type u} (s t : Set α), s ∩ t ∪ s \ t = s The theorem `Set.inter_union_diff` states that for any type `α` and any sets `s` and `t` of type `α`, the union of the intersection of `s` and `t` and the difference of `s` and `t` is equal to `s`. In other words, if we take the common elements of `s` and `t` (i.e., `s ∩ t`), and unite them with the elements that are in `s` but not in `t` (i.e., `s \ t`), we get back the set `s`. This is expressed in terms of set operations, and is a restatement of a standard identity in set theory. More concisely: The theorem `Set.inter_union_diff` asserts that for any set `α` and sets `s` and `t` in `α`, `s = (s ∩ t) ∪ (s \ t)`.
`Set.union_diff_left` theorem Set.union_diff_left : ∀ {α : Type u} {s t : Set α}, (s ∪ t) \ s = t \ s The theorem `Set.union_diff_left` states that for any type `α` and any two sets `s` and `t` of type `α`, the difference of the union of `s` and `t` and `s` is equal to the difference of `t` and `s`. In other words, if you take the union of two sets and then remove the elements of one of the sets, you end up with the same result as if you just removed the elements of that set from the other set to begin with: $(s \cup t) \setminus s = t \setminus s$. More concisely: The theorem `Set.union_diff_left` asserts that for any sets `s` and `t` of type `α`, the difference between `s` and the set difference of `s` and `t` is equal to the set difference of `t` and `s`, that is, `s \ ((s \cup t)) = t \ s`.
`Set.nonempty_iff_ne_empty'` theorem Set.nonempty_iff_ne_empty' : ∀ {α : Type u} {s : Set α}, Nonempty ↑s ↔ s ≠ ∅ This theorem, `Set.nonempty_iff_ne_empty'`, states that for any type `α` and any set `s` of type `α`, it holds that `s` is nonempty if and only if `s` is not equal to the empty set. In other words, it provides a condition to check whether a set `s` contains at least one element or not. It is equivalent to say that a set is nonempty or it is not the empty set. More concisely: A set is nonempty if and only if it is not equal to the empty set.
`Set.nonempty_iff_univ_nonempty` theorem Set.nonempty_iff_univ_nonempty : ∀ {α : Type u}, Nonempty α ↔ Set.univ.Nonempty This theorem, `Set.nonempty_iff_univ_nonempty`, establishes an equivalence between two properties for any given type `α`. The first property, `Nonempty α`, states that there exists an instance of the type `α`, i.e., the type `α` is nonempty. The second property, `Set.Nonempty Set.univ`, asserts that the universal set over the type `α`, which contains all elements of `α`, is nonempty. In essence, it says that a type `α` has an instance if and only if its universal set is not empty. More concisely: A set is nonempty if and only if its universal set is nonempty.
`Mathlib.Data.Set.Basic._auxLemma.81` theorem Mathlib.Data.Set.Basic._auxLemma.81 : ∀ {α : Type u} {s t u : Set α}, (s ⊆ t \ u) = (s ⊆ t ∧ Disjoint s u) := by sorry This theorem states that for any type `α` and any sets `s`, `t`, and `u` of type `α`, the statement "the set `s` is a subset of the difference of sets `t` and `u`" is equivalent to the conjunction of two statements: "the set `s` is a subset of `t`" and "the set `s` is disjoint with `u`". Here, two sets are called disjoint if their intersection is the empty set. More concisely: For any type `α` and sets `s`, `t`, and `u` of type `α`, the set `s` is a subset of `t - u` if and only if `s` is a subset of `t` and `s` is disjoint with `u`.
`Set.Nonempty.empty_ssubset` theorem Set.Nonempty.empty_ssubset : ∀ {α : Type u} {s : Set α}, s.Nonempty → ∅ ⊂ s This theorem, referred to as an alias of the reverse direction of `Set.empty_ssubset`, states that for any type `α` and any set `s` of this type, if `s` is nonempty, then the empty set is a strict subset of `s`. This means that the empty set is a subset of `s` but is not equal to `s`. More concisely: If `s` is a nonempty set, then the empty set is a proper subset of `s`.
`AntitoneOn.inter` theorem AntitoneOn.inter : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder β] {f g : β → Set α} {s : Set β}, AntitoneOn f s → AntitoneOn g s → AntitoneOn (fun x => f x ∩ g x) s The theorem `AntitoneOn.inter` states that for any types `α` and `β`, where `β` has a preorder, and any functions `f` and `g` from `β` to sets of `α`, and a set `s` of `β`, if both `f` and `g` are antitone (meaning reversely ordered) on `s`, then the function that maps each element of `β` to the intersection of the sets `f(x)` and `g(x)` is also antitone on `s`. This means that for all elements `a` and `b` in `s`, if `a ≤ b` then the intersection of the sets at `b` is a subset of the intersection of the sets at `a`. More concisely: If `f` and `g` are antitone functions from a preordered set `β` to sets of a type `α`, then their intersection function, which maps each element `x` in `β` to the intersection of `f(x)` and `g(x)`, is also an antitone function on `β`. In other words, for all `a, b` in `β` with `a ≤ b`, we have `∩(f a) ⊆ ∩(f b)`.
`Set.eq_empty_of_forall_not_mem` theorem Set.eq_empty_of_forall_not_mem : ∀ {α : Type u} {s : Set α}, (∀ (x : α), x ∉ s) → s = ∅ This theorem states that for any type `α` and any set `s` of elements of that type, if every element of `α` is not a member of `s`, then `s` must be equivalent to the empty set. In other words, if no element belongs to the set `s`, it is identical to the empty set. This is a fundamental property of sets in mathematics. More concisely: If a set `s` of type `α` contains no elements of `α`, then `s` is equivalent to the empty set.
`Set.union_eq_self_of_subset_right` theorem Set.union_eq_self_of_subset_right : ∀ {α : Type u} {s t : Set α}, t ⊆ s → s ∪ t = s The theorem `Set.union_eq_self_of_subset_right` states that for all types `α` and for any two sets `s` and `t` of type `α`, if `t` is a subset of `s`, then the union of `s` and `t` is equal to `s`. This means that adding all elements from `t` to `s` does not change the set `s`, which is a direct consequence of the fact that all elements of `t` are already in `s` because `t` is a subset of `s`. More concisely: For all types `α` and sets `s` and `t` of type `α`, if `t` is a subset of `s`, then `s = s ∪ t`.
`Set.eq_empty_of_isEmpty` theorem Set.eq_empty_of_isEmpty : ∀ {α : Type u} [inst : IsEmpty α] (s : Set α), s = ∅ The theorem `Set.eq_empty_of_isEmpty` states that for any type `α`, if `α` is an empty type (i.e., there are no elements of type `α`), then any set `s` of type `α` is necessarily equal to the empty set. This follows because there are no elements to include in the set `s`. More concisely: If a type `α` is empty, then any set `s` of type `α` is the empty set.
`Disjoint.ne_of_mem` theorem Disjoint.ne_of_mem : ∀ {α : Type u} {s t : Set α}, Disjoint s t → ∀ ⦃a : α⦄, a ∈ s → ∀ ⦃b : α⦄, b ∈ t → a ≠ b The theorem `Disjoint.ne_of_mem` states that for any two sets `s` and `t` of type `α`, if the sets `s` and `t` are disjoint, then for any elements `a` from `s` and `b` from `t`, the elements `a` and `b` must be distinct. This is an alias of the forward direction of the theorem `Set.disjoint_iff_forall_ne`. It generalizes the principle that in a set theoretical context, disjoint sets have no elements in common. More concisely: If sets `s` and `t` are disjoint, then for all `a ∈ s` and `b ∈ t`, `a ≠ b`.
`Set.mem_singleton` theorem Set.mem_singleton : ∀ {α : Type u} (a : α), a ∈ {a} This theorem, `Set.mem_singleton`, states that for any type `α` and any element `a` of type `α`, `a` is a member of the set that contains only `a`. In other words, `a` is an element of the singleton set `{a}`. More concisely: For any type `α` and element `a` of type `α`, `a` is an element of the singleton set `{a}`. Equivalently, the singleton set `{a}` contains `a` as an element.
`Set.disjoint_compl_right_iff_subset` theorem Set.disjoint_compl_right_iff_subset : ∀ {α : Type u} {s t : Set α}, Disjoint s tᶜ ↔ s ⊆ t The theorem `Set.disjoint_compl_right_iff_subset` states that for any two sets `s` and `t` of some type `α`, the set `s` and the complement of set `t` (`tᶜ`) are disjoint if and only if `s` is a subset of `t`. In other words, `s` shares no common element with the complement of `t` exactly when every element in `s` is also an element of `t`. This theorem generalizes the concept of disjoint sets in the context of lattices. More concisely: For sets `s` and `t` in type `α`, `s` is disjoint with the complement of `t` if and only if `s` is a subset of `t`.
`Mathlib.Data.Set.Basic._auxLemma.49` theorem Mathlib.Data.Set.Basic._auxLemma.49 : ∀ {α : Type u} (a : α), {a}.Nonempty = True This theorem states that for any type `α` and any element `a` of type `α`, the singleton set containing just `a` is indeed non-empty. This means that there exists an element in the set that contains only `a`, which is unsurprising as `a` itself is the element in it. More concisely: For any type `α` and any of its element `a`, the singleton set `{a : α}` is a non-empty set.
`Set.inter_union_compl` theorem Set.inter_union_compl : ∀ {α : Type u} (s t : Set α), s ∩ t ∪ s ∩ tᶜ = s This theorem states that for any type `α` and any two sets `s` and `t` of type `α`, the union of the intersection of `s` and `t` with the intersection of `s` and the complement of `t` equals `s`. In mathematical notation, this can be written as $s \cap t \cup s \cap t^c = s$. This theorem essentially captures the idea that if we take a set `s` and intersect it with another set `t`, and also intersect it with the complement of `t`, and then take the union of these two intersections, we essentially recover the original set `s`. More concisely: The theorem asserts that for any set `s` of type `α`, the union of `s` intersected with `t` and `s` intersected with the complement of `t` equals `s`, i.e., `s ∩ t ∪ s ∩ t^c = s`.
`Set.empty_ne_univ` theorem Set.empty_ne_univ : ∀ {α : Type u} [inst : Nonempty α], ∅ ≠ Set.univ This theorem states that for any non-empty type `α`, the empty set is not equal to the universal set. In other words, for all types `α` that have at least one element, the set that contains no elements (`∅`) is not the same as the set that contains all elements of `α` (`Set.univ`). More concisely: For any non-empty type `α`, the empty set `∅` is a proper subset of the universal set `Set.univ`.
`LE.le.subset` theorem LE.le.subset : ∀ {α : Type u} {s t : Set α}, s ≤ t → s ⊆ t The theorem `LE.le.subset` states that for any type `α` and any two sets `s` and `t` of type `α`, if `s` is less than or equal to `t` (denoted by `s ≤ t`), then `s` is a subset of `t`. Here, the symbol '⊆' represents the subset relation. In other words, every element of set `s` is also an element of set `t`. This theorem is an alias for the forward direction of another theorem, `Set.le_iff_subset`. More concisely: If `s` is a set that is less than or equal to `t` (`s ≤ t`), then `s` is a subset of `t` (`s ⊆ t`).
`Set.disjoint_left` theorem Set.disjoint_left : ∀ {α : Type u} {s t : Set α}, Disjoint s t ↔ ∀ ⦃a : α⦄, a ∈ s → a ∉ t This theorem, `Set.disjoint_left`, states that for any type `α` and any two sets `s` and `t` of `α`, `s` and `t` are disjoint (in the sense that their greatest lower bound is the bottom element) if and only if for every element `a` of type `α`, if `a` is an element of set `s` then `a` is not an element of set `t`. In other words, two sets are disjoint if no element of the first set is an element of the second set. More concisely: Two sets of the same type have no elements in common if and only if their intersection is the empty set.
`Set.insert_eq` theorem Set.insert_eq : ∀ {α : Type u} (x : α) (s : Set α), insert x s = {x} ∪ s This theorem states that for any type `α`, any element `x` of type `α`, and any set `s` of elements of type `α`, the set obtained by inserting the element `x` into the set `s` is equal to the union of the singleton set containing `x` and the set `s`. In other words, adding an element to a set can also be seen as taking the union of the original set with a new set that contains only the element to be added. More concisely: For any type `α`, and for any set `s` of elements from `α` and any element `x` in `α`, the set `{x} ∪ s` equals `{x} ⋃ s`. (Here, `{x}` denotes the singleton set containing `x`.)
`Set.compl_union` theorem Set.compl_union : ∀ {α : Type u} (s t : Set α), (s ∪ t)ᶜ = sᶜ ∩ tᶜ This theorem, `Set.compl_union`, states that for all types `α`, and for any two sets `s` and `t` of this type, the complement of the union of `s` and `t` is equal to the intersection of the complement of `s` and the complement of `t`. In mathematical terms, this can be written as $(s \cup t)^c = s^c \cap t^c$. This is a fundamental theorem in set theory that reflects the relationship between union, intersection, and complement operations in sets. More concisely: The complement of the union of two sets is equal to the intersection of their complements: $(s \cup t)^c = s^c \cap t^c$.
`Set.union_compl_self` theorem Set.union_compl_self : ∀ {α : Type u} (s : Set α), s ∪ sᶜ = Set.univ This theorem states that for any set `s` of a given type `α`, the union of `s` and its complement `sᶜ` is the universal set. In other words, every element of type `α` is either in `s` or in the complement of `s`, and hence the union of `s` and `sᶜ` covers all of `α`, i.e., it is the universal set. This is a formalization of the basic principle from set theory that a set combined with its complement yields the entire universe of discourse. In mathematical notation, this is often written as $s \cup s^c = U$, where $U$ represents the universal set, $s$ is any subset of $U$, and $s^c$ is the complement of $s$ in $U$. More concisely: For any set `s` of type `α`, the union of `s` and its complement `sᶜ` equals the universal set `U` of type `α`. In Lean notation, `s ∪ sᶜ = U`.
`Set.insert_eq_of_mem` theorem Set.insert_eq_of_mem : ∀ {α : Type u} {a : α} {s : Set α}, a ∈ s → insert a s = s This theorem states that for any type `α`, any element `a` of type `α`, and any set `s` of type `α`, if `a` is an element of `s` (i.e., `a ∈ s`), then inserting `a` into `s` does not change `s`. In other words, inserting an element into a set, where the element is already a member of the set, leaves the set unchanged. More concisely: For any type `α`, any set `s` of type `α`, and any element `a` in `s`, the set `insert a s` equals `s`.
`Set.singleton_union` theorem Set.singleton_union : ∀ {α : Type u} {a : α} {s : Set α}, {a} ∪ s = insert a s The theorem `Set.singleton_union` states that for any given type `α`, an element `a` of type `α`, and a set `s` of type `Set α`, the union of the singleton set containing `a` (denoted as `{a}`) and the set `s` is equal to the set obtained by inserting `a` into `s`. In other words, the union of a singleton set and another set can be created by simply adding the single element to the other set. More concisely: For any type `α`, set `s` of type `Set α`, and element `a` of type `α`, `{a} ∪ s = s.insert a`.
`Mathlib.Data.Set.Basic._auxLemma.28` theorem Mathlib.Data.Set.Basic._auxLemma.28 : ∀ {α : Type u} {s t r : Set α}, (r ⊆ s ∩ t) = (r ⊆ s ∧ r ⊆ t) This theorem states that for any type `α`, and any sets `s`, `t`, and `r` of type `α`, the property of `r` being a subset of the intersection of `s` and `t` is equivalent to `r` being a subset of `s` and `r` being a subset of `t`. In terms of set theory, this expresses the fact that a subset of the intersection of two sets is also a subset of each of the intersecting sets. More concisely: For any type `α` and sets `s`, `t` of type `α`, `r ⊆ s ∩ t` if and only if `r ⊆ s` and `r ⊆ t`.
`Mathlib.Data.Set.Basic._auxLemma.65` theorem Mathlib.Data.Set.Basic._auxLemma.65 : ∀ {a b : Prop}, (¬(a ∧ b)) = (a → ¬b) The theorem `Mathlib.Data.Set.Basic._auxLemma.65` states that for any two propositions `a` and `b`, the negation of the conjunction of `a` and `b` is logically equivalent to the implication from `a` to the negation of `b`. In other words, saying "it's not true that both `a` and `b` are true" is the same as saying "if `a` is true, then `b` must not be true". More concisely: The negation of `a` conjunction `b` is logically equivalent to `a` implying `~b`.
`Set.inter_empty` theorem Set.inter_empty : ∀ {α : Type u} (a : Set α), a ∩ ∅ = ∅ The theorem `Set.inter_empty` states that for all types `α` and for any set `a` of type `α`, the intersection of `a` with the empty set is the empty set. In mathematical terms, for any set `A`, we have `A ∩ ∅ = ∅`. This means that there are no elements which belong to both `A` and the empty set, which is consistent with the definition of set intersection. More concisely: For any set `A`, the intersection of `A` with the empty set is the empty set. In mathematical notation, `A ∩ ∅ = ∅`.
`Set.mem_compl` theorem Set.mem_compl : ∀ {α : Type u} {s : Set α} {x : α}, x ∉ s → x ∈ sᶜ This theorem states that for any type 'α', any set 's' of type 'α', and any element 'x' of type 'α', if 'x' is not an element of 's', then 'x' is an element of the complement of 's'. Here, the complement of a set 's' (denoted as 'sᶜ' in Lean 4) refers to all elements of type 'α' that are not in 's'. More concisely: If x is not an element of set s, then x belongs to the complement of s.
`Set.union_subset` theorem Set.union_subset : ∀ {α : Type u} {s t r : Set α}, s ⊆ r → t ⊆ r → s ∪ t ⊆ r The theorem `Set.union_subset` states that for any type `α`, and any three sets `s`, `t`, and `r` of type `α`, if set `s` is a subset of set `r` and set `t` is also a subset of set `r`, then the union of set `s` and set `t` is also a subset of set `r`. This mimics the basic property of sets in mathematics: the union of two subsets of a set is always a subset of that set. More concisely: If sets `s` and `t` are subsets of set `r` in type `α`, then their union `s ∪ t` is also a subset of `r`.
`Set.nonempty_of_nonempty_subtype` theorem Set.nonempty_of_nonempty_subtype : ∀ {α : Type u} {s : Set α} [inst : Nonempty ↑s], s.Nonempty This theorem, named `Set.nonempty_of_nonempty_subtype`, states that for any type `α` and any set `s` of type `α`, if the subtype induced by `s` is nonempty (i.e., there exists an element in `s`), then the set `s` itself is nonempty. In other words, if we can find an element within the subset of the universe defined by `s`, it implies that `s` is not an empty set. The proof of this theorem is not provided here. More concisely: If a subtype of a type `α` is nonempty, then the underlying set is nonempty.
`Mathlib.Data.Set.Basic._auxLemma.83` theorem Mathlib.Data.Set.Basic._auxLemma.83 : ∀ {α : Type u} {s : Set α}, (sᶜ = Set.univ) = (s = ∅) The theorem `Mathlib.Data.Set.Basic._auxLemma.83` states that for any type `α` and any set `s` of this type, the complement of `s` is equal to the universal set if and only if `s` itself is the empty set. Here, `Set.univ` stands for the universal set (i.e., the set containing all elements of the type `α`), `sᶜ` represents the complement of a set `s`, and `∅` represents the empty set. The theorem basically emphasizes the set theory principle that the complement of an empty set is the universal set, and vice versa. More concisely: For any type α, the complement of an empty set is the universal set, and the empty set is the complement of the universal set.
`Set.sep_eq_self_iff_mem_true` theorem Set.sep_eq_self_iff_mem_true : ∀ {α : Type u} {s : Set α} {p : α → Prop}, {x \| x ∈ s ∧ p x} = s ↔ ∀ x ∈ s, p x This theorem states that for any type `α`, a set `s` of `α`, and a property `p` that each element of `α` may or may not satisfy, the set of elements `x` such that `x` is in `s` and `x` satisfies `p` is equal to `s` if and only if every element in `s` satisfies `p`. In mathematical terms, it claims that ${x \| x \in s \land p(x)} = s$ if and only if for all $x \in s$, $p(x)$ is true. More concisely: For any set `s` of type `α` and property `p` on `α`, `{x \| x ∈ s ∧ p(x)} = s` if and only if for all `x ∈ s`, `p(x)` holds.
`Set.Nonempty.not_disjoint` theorem Set.Nonempty.not_disjoint : ∀ {α : Type u} {s t : Set α}, (s ∩ t).Nonempty → ¬Disjoint s t This theorem states that for any two sets `s` and `t` of some type `α`, if the intersection of `s` and `t` is nonempty, then `s` and `t` are not disjoint. In other words, if there exists an element that belongs to both `s` and `t`, then it is not true that every element that is less than or equal to `s` and less than or equal to `t` is also less than or equal to the bottom element of the lattice, where the lattice and the order relation are defined with respect to the type `α`. This theorem is a negation or reverse direction of the lemma `Set.not_disjoint_iff_nonempty_inter`. More concisely: If two sets `s` and `t` of type `α` have a nonempty intersection, then there exists an element in `s ∩ t` that is not the bottom element of the lattice on `α`.
`Disjoint.subset_compl_left` theorem Disjoint.subset_compl_left : ∀ {α : Type u} {s t : Set α}, Disjoint t s → s ⊆ tᶜ This theorem, referred to as `Disjoint.subset_compl_left`, states that for any type `α` and for any two sets `s` and `t` of this type, if `t` and `s` are disjoint, then `s` is a subset of the complement of `t` (denoted as `tᶜ`). In other words, if no element of `s` is also an element of `t`, then every element of `s` must be in the set of elements which are not in `t`. More concisely: If sets `s` and `t` are disjoint, then `s` is a subset of `tᵜ` (the complement of `t`).
`Mathlib.Data.Set.Basic._auxLemma.31` theorem Mathlib.Data.Set.Basic._auxLemma.31 : ∀ {α : Type u} {s t : Set α}, (s = s ∩ t) = (s ⊆ t) This theorem is stating that for any type `α` and any two sets `s` and `t` of type `α`, the set `s` is equal to the intersection of `s` and `t` if and only if `s` is a subset of `t`. In other words, every element of `s` is also an element of `t`. This can be expressed mathematically as `s = s ∩ t ⇔ s ⊆ t` for all sets `s` and `t`. More concisely: For any sets `s` and `t` of type `α`, `s = s ∩ t` if and only if `s ⊆ t`.
`Set.singleton_ne_empty` theorem Set.singleton_ne_empty : ∀ {α : Type u} (a : α), {a} ≠ ∅ This theorem declares that a set containing a single element is not equal to an empty set. For any type `α` and any element `a` of that type, the singleton set `{a}` cannot be equal to an empty set `∅`. In essence, a set with at least one element is always distinct from an empty set. More concisely: For any type `α` and any element `a` of type `α`, the singleton set `{a}` is not equal to the empty set `∅`.
`Set.pair_eq_singleton` theorem Set.pair_eq_singleton : ∀ {α : Type u} (a : α), {a, a} = {a} This theorem states that for all types `α` and for all elements `a` of type `α`, the set that contains `a` twice is equal to the set that contains `a` once. In other words, in set notation, a set with repeated elements is equivalent to the same set where the repeated elements are only listed once. More concisely: For all types `α` and all elements `a` of type `α`, the set `{a, a} = {a}`.
`Set.inter_comm` theorem Set.inter_comm : ∀ {α : Type u} (a b : Set α), a ∩ b = b ∩ a This theorem, `Set.inter_comm`, states that for all types `α` and sets `a` and `b` of type `α`, the intersection of `a` and `b` is equal to the intersection of `b` and `a`. In other words, the order in which the sets are intersected does not matter, demonstrating the commutative property of intersection. In mathematical notation, this is equivalent to saying for all sets `a` and `b`, `a ∩ b = b ∩ a`. More concisely: The theorem asserts that for all types `α` and sets `a` and `b` of type `α`, the intersection `a ∩ b` is equal to the intersection `b ∩ a`.
`Set.inter_self` theorem Set.inter_self : ∀ {α : Type u} (a : Set α), a ∩ a = a The theorem `Set.inter_self` states that for all types `α`, and for any set `a` of type `α`, the intersection of the set `a` with itself is equal to the set `a`. This is a reflection of the intuitive concept in set theory where the intersection of a set with itself will obviously yield the original set since all elements in the set are common to the set itself. More concisely: For any set `a` of type `α`, `a ∩ a = a`.
`Set.insert_subset_insert` theorem Set.insert_subset_insert : ∀ {α : Type u} {a : α} {s t : Set α}, s ⊆ t → insert a s ⊆ insert a t This theorem states that for any type `α`, an element `a` of type `α`, and two sets `s` and `t` of type `α`, if set `s` is a subset of set `t`, then the set resulting from inserting element `a` into `s` is a subset of the set resulting from inserting `a` into `t`. Essentially, it explains how the subset relation is preserved when the same element is added to both the subset and its superset. More concisely: For any type `α`, sets `s` and `t` of type `α` with `s ⊆ t`, and element `a` of type `α`, we have `insert a s ⊆ insert a t`.
`Set.inter_eq_left` theorem Set.inter_eq_left : ∀ {α : Type u} {s t : Set α}, s ∩ t = s ↔ s ⊆ t This theorem, named `Set.inter_eq_left`, states that for any type `α` and any two sets `s` and `t` of that type, the intersection of `s` and `t` is equal to `s` if and only if `s` is a subset of `t`. In other words, it shows a logical equivalence between "the intersection of two sets being one of those sets" and "that set being a subset of the other set". This theorem holds true for all possible types `α` and all possible sets `s` and `t` of that type. More concisely: For any type α and sets s and t of type α, s ∩ t = s if and only if s ⊆ t.
`Set.diff_eq_compl_inter` theorem Set.diff_eq_compl_inter : ∀ {α : Type u} {s t : Set α}, s \ t = tᶜ ∩ s This theorem states that for any two sets `s` and `t` of the same type `α`, the difference of `s` and `t`, denoted by `s \ t`, is equivalent to the intersection of the complement of `t` and `s`. In other words, removing all elements of `t` from `s` is the same as taking the intersection of `s` with all the elements that are not in `t`. More concisely: For sets `s` and `t` of type `α` in Lean 4, `s \ t` is equivalent to `s ∩ COMPLEMENT t`.
`Set.not_nonempty_empty` theorem Set.not_nonempty_empty : ∀ {α : Type u}, ¬∅.Nonempty This theorem, "Set.not_nonempty_empty", states that for all types `α`, the empty set is not non-empty. In other words, there doesn't exist any element in the empty set. It is a formal way to express that the property `Set.Nonempty` is not satisfied by the empty set, symbolized as `∅` in mathematics. This is a fundamental property of empty sets in set theory. More concisely: The empty set is not non-emptier. (In other words, the property of being non-empty is not satisfied by the empty set.)
`Set.eq_univ_iff_forall` theorem Set.eq_univ_iff_forall : ∀ {α : Type u} {s : Set α}, s = Set.univ ↔ ∀ (x : α), x ∈ s This theorem states that for any type `α` and any set `s` of type `Set α`, `s` is equal to the universal set `Set.univ` if and only if every element `x` of type `α` belongs to `s`. In other words, a set is the universal set if it contains all possible elements of its underlying type. More concisely: A set `s` of type `α` is equal to the universal set `Set.univ` if and only if `x ∈ s` for all `x : α`.
`Set.not_disjoint_iff_nonempty_inter` theorem Set.not_disjoint_iff_nonempty_inter : ∀ {α : Type u} {s t : Set α}, ¬Disjoint s t ↔ (s ∩ t).Nonempty The theorem `Set.not_disjoint_iff_nonempty_inter` asserts that for all types `α` and for all sets `s` and `t` of this type, `s` and `t` are not disjoint if and only if the intersection of `s` and `t` is nonempty. Here, two sets are considered disjoint if their intersection is empty. Therefore, this theorem is stating that the negation of the disjointness of two sets is equivalent to the non-emptiness of their intersection. More concisely: A sets `s` and `t` are not disjoint if and only if their intersection is non-empty. (In other words, sets `s` and `t` have non-empty intersection if and only if they are not disjoint.)
`HasSubset.Subset.disjoint_compl_right` theorem HasSubset.Subset.disjoint_compl_right : ∀ {α : Type u} {s t : Set α}, s ⊆ t → Disjoint s tᶜ This theorem, called `HasSubset.Subset.disjoint_compl_right`, asserts that for any two sets `s` and `t` of any type `α`, if set `s` is a subset of set `t`, then `s` and the complement of `t` are disjoint. In other words, there are no common elements between set `s` and the complement of set `t`. Here, 'complement' refers to the set of all elements of type `α` that are not in `t`, and 'disjoint' means that the greatest element shared by both `s` and `tᶜ` is the bottom element of the partial order, i.e., there is no element common to both sets. More concisely: If `s` is a subset of `t`, then `s` and the complement of `t` have no common elements.
`Set.inter_eq_right` theorem Set.inter_eq_right : ∀ {α : Type u} {s t : Set α}, s ∩ t = t ↔ t ⊆ s This theorem, `Set.inter_eq_right`, states that for any type `α` and any two sets `s` and `t` of type `α`, the intersection of `s` and `t` is equal to `t` if and only if `t` is a subset of `s`. In mathematical terms, given any two sets `s` and `t`, we have that `s ∩ t = t` is equivalent to `t ⊆ s`. This theorem captures one of the fundamental properties of the intersection operation in set theory. More concisely: The intersection of two sets is equal to the smaller set if and only if the smaller set is a subset of the larger set. (i.e., `s ∩ t = t` if and only if `t ⊆ s`).
`Set.not_nonempty_iff_eq_empty` theorem Set.not_nonempty_iff_eq_empty : ∀ {α : Type u} {s : Set α}, ¬s.Nonempty ↔ s = ∅ This theorem, `Set.not_nonempty_iff_eq_empty`, establishes the equivalence between the non-existence of a nonempty set `s` of a certain type `α`, denoted as `¬Set.Nonempty s`, and the set `s` being an empty set, denoted as `s = ∅`. This means that for any given set `s`, it is not nonempty if and only if it is an empty set. It suggests that if no elements exist in the set `s` (i.e., the set `s` is not nonempty), then the set `s` is indeed an empty set, and vice versa. This theorem is a formalization of a fundamental concept in set theory. More concisely: The theorem asserts that a set `s` of type `α` is nonempty if and only if it is not equal to the empty set `∅`.
`Set.diff_inter_self_eq_diff` theorem Set.diff_inter_self_eq_diff : ∀ {α : Type u} {s t : Set α}, s \ (t ∩ s) = s \ t This theorem states that for any set `s` and `t` of some type `α`, the difference of `s` with the intersection of `t` and `s` is equal to the difference of `s` and `t`. That is, removing the elements that both `s` and `t` have from `s` is the same as just removing the elements of `t` from `s`. In mathematical notation, this is denoted as $s \setminus (t \cap s) = s \setminus t$. More concisely: The theorem asserts that for any set `s` and `t` of type `α`, their set difference `s \ (t ∩ s)` equals `s \ t`.
`Set.compl_subset_comm` theorem Set.compl_subset_comm : ∀ {α : Type u} {s t : Set α}, sᶜ ⊆ t ↔ tᶜ ⊆ s This theorem states that for any type `α` and any two sets `s` and `t` of `α`, the complement of `s` is a subset of `t` if and only if the complement of `t` is a subset of `s`. In other words, it articulates the commutativity of the subset relation between the complements of two sets. More concisely: For any type `α` and sets `s` and `t` of `α`, the complements `complement s` and `complement t` are equal if and only if sets `s` and `t` are subsets of each other. (Note: In Lean, `complement s` denotes the set of elements not in `s`.)
`Set.union_subset_iff` theorem Set.union_subset_iff : ∀ {α : Type u} {s t u : Set α}, s ∪ t ⊆ u ↔ s ⊆ u ∧ t ⊆ u This theorem, `Set.union_subset_iff`, states that for any type `α` and any sets `s`, `t`, and `u` of type `α`, the set `s` union with the set `t` is a subset of set `u` if and only if both sets `s` and `t` are subsets of `u`. In mathematical terms, we would express this as $s \cup t \subseteq u \Leftrightarrow (s \subseteq u) \land (t \subseteq u)$. It means that the union of two sets is contained within another set precisely when both of the constituent sets are contained within that other set. More concisely: For sets `s`, `t`, and `u` of type `α`, `s ∪ t ⊆ u` if and only if `s ⊆ u` and `t ⊆ u`.
`Set.compl_univ` theorem Set.compl_univ : ∀ {α : Type u}, Set.univᶜ = ∅ This theorem states that the complement of the universal set in any type `α` is the empty set. In other words, there is no element in the type `α` that is not in the universal set, hence the set of all such elements, denoted as the complement of the universal set (`Set.univᶜ`), is indeed the empty set (`∅`). This is a fundamental concept in set theory. More concisely: The complement of the universal set in any type `α` is the empty set. Mathematically: `Set.univᶜ : ∀ {α : Type}, Set α = ∅`
`Set.sep_subset` theorem Set.sep_subset : ∀ {α : Type u} (s : Set α) (p : α → Prop), {x \| x ∈ s ∧ p x} ⊆ s The theorem `Set.sep_subset` states that for any type `α`, any set `s` of type `α`, and any predicate `p` on `α`, the subset of `s` consisting of elements that satisfy the predicate `p` is a subset of `s`. In other words, if we filter a set based on some condition, the resulting set is always a subset of the original set. This is a fundamental result about subsets and predicates in set theory. More concisely: For any type `α`, set `s` of `α`, and predicate `p` on `α`, `{x : α \| p x} ⊆ s`.
`Mathlib.Data.Set.Basic._auxLemma.30` theorem Mathlib.Data.Set.Basic._auxLemma.30 : ∀ {α : Type u} {s t : Set α}, (s ∩ t = t) = (t ⊆ s) This theorem states that for any two sets `s` and `t` of a certain type `α`, the intersection of `s` and `t` being equal to `t` is equivalent to `t` being a subset of `s`. In other words, `t` is a subset of `s` if and only if every element in `t` also belongs to `s`, resulting in the intersection of `s` and `t` to be `t` itself. More concisely: For sets `s` and `t` of type `α`, `s` contains `t`, i.e., `t ⊆ s`, if and only if the intersection of `s` and `t` equals `t`, i.e., `s ∩ t = t`.
`Set.subset_union_right` theorem Set.subset_union_right : ∀ {α : Type u} (s t : Set α), t ⊆ s ∪ t This theorem, `Set.subset_union_right`, states that for any type `α` and any two sets `s` and `t` of type `α`, `t` is a subset of the union of `s` and `t`. In other words, all elements of `t` are also elements of the union of `s` and `t`. This is a basic property of sets and union operation: any set is always a subset of the union of itself with another set. More concisely: For any types `α` and sets `s` and `t` of type `α`, `t` is a subset of `s ∪ t`.
`Set.univ_eq_empty_iff` theorem Set.univ_eq_empty_iff : ∀ {α : Type u}, Set.univ = ∅ ↔ IsEmpty α This theorem states that for any type `α`, the universal set of `α` is equivalent to an empty set if and only if `α` is an empty type. Here, the universal set of `α` is the set that contains all elements of the type `α`. The term `IsEmpty α` indicates that the type `α` has no elements, i.e., it's an 'empty type'. So, essentially, this theorem establishes a connection between a type being empty and its universal set being an empty set. More concisely: For any type `α`, the universal set of `α` is equal to the empty set if and only if `α` is an empty type.
`Set.eq_univ_of_subset` theorem Set.eq_univ_of_subset : ∀ {α : Type u} {s t : Set α}, s ⊆ t → s = Set.univ → t = Set.univ This theorem states that for any type `α` and any two sets `s` and `t` of this type, if `s` is a subset of `t` and `s` is equivalent to the universal set on `α` (`Set.univ`), then `t` must also be equivalent to the universal set. In other words, if all elements of `α` are in `s` and `s` is included in `t`, then all elements of `α` must also be in `t`. More concisely: If a subset `s` of type `α` is equal to the universal set `Set.univ` on `α` and is contained in another set `t` of type `α`, then `t` is also equal to `Set.univ` on `α`.
`Set.ssubset_iff_insert` theorem Set.ssubset_iff_insert : ∀ {α : Type u} {s t : Set α}, s ⊂ t ↔ ∃ a ∉ s, insert a s ⊆ t This theorem states that for any arbitrary type `α`, and any two sets `s` and `t` of type `α`, `s` is a proper subset of `t` if and only if there exists an element `a` not in `s` such that inserting `a` into `s` results in a set that is a subset of `t`. In other words, `s` is a proper subset of `t` precisely when `t` contains `s` and at least one additional element not in `s`. More concisely: A set `s` is a proper subset of `t` if and only if `t` contains `s` and there exists an element not in `s` that belongs to `t`.
`SetCoe.forall` theorem SetCoe.forall : ∀ {α : Type u} {s : Set α} {p : ↑s → Prop}, (∀ (x : ↑s), p x) ↔ ∀ (x : α) (h : x ∈ s), p ⟨x, h⟩ This theorem, named `SetCoe.forall`, asserts that for all types `α` and for all sets `s` of type `α`, and any predicate `p` that applies to elements of the set `s`, it is equivalent to say that the predicate `p` holds for all elements of `s` and to say that for all elements `x` of type `α`, if `x` is in the set `s`, then the predicate `p` holds for `x` with the evidence that `x` is in `s`. Essentially, it is expressing the property of universal quantification over the elements of a set in two different ways. More concisely: For any type `α`, set `s` of `α`, and predicate `p` on `α`, the statements "for all `x` in `s`, `p(x)` holds" and "for all `x` in `α` with `x` in `s`, `p(x)` holds" are equivalent.
`Mathlib.Data.Set.Basic._auxLemma.1` theorem Mathlib.Data.Set.Basic._auxLemma.1 : ∀ {α : Type u} {p q : α → Prop}, ({a \| p a} ⊆ {a \| q a}) = ∀ (a : α), p a → q a This theorem, `Mathlib.Data.Set.Basic._auxLemma.1`, from the Lean Mathematical Library's basic set theory module, states that for any type `α` and for any two properties `p` and `q` which apply to elements of type `α`, the set of elements of `α` for which `p` holds is a subset of the set of elements for which `q` holds if and only if every element of `α` that satisfies `p` also satisfies `q`. In mathematical notation, this can be written as: `{a ∈ α \| p(a)} ⊆ {a ∈ α \| q(a)}` if and only if `∀a ∈ α, p(a) → q(a)`. More concisely: For any type `α` and properties `p` and `q` of its elements, `{a ∈ α \| p(a)}` is a subset of `{a ∈ α \| q(a)}` if and only if for all `a` in `α`, `p(a)` implies `q(a)`.
`Set.setOf_mem_eq` theorem Set.setOf_mem_eq : ∀ {α : Type u} {s : Set α}, {x \| x ∈ s} = s This theorem states that for all types `α` and for all sets `s` of type `α`, the set of all elements `x` such that `x` is a member of `s` is equal to `s` itself. In other words, if we construct a set by collecting all the elements from a given set, we end up with the original set. This is a fundamental property of sets that is being formally stated and proven in the Lean 4 theorem prover. More concisely: For all types `α` and sets `s` of type `α`, `s` is equal to the set of its elements.
`Mathlib.Data.Set.Basic._auxLemma.76` theorem Mathlib.Data.Set.Basic._auxLemma.76 : ∀ {α : Type u} {s : Set α}, Disjoint s Set.univ = (s = ∅) This theorem states that for any type `α` and any set `s` of type `α`, `s` is disjoint with the universal set if and only if `s` is the empty set. To elaborate, two elements of a lattice are called disjoint if their infimum is the bottom element. Here, it refers to the condition where a set `s` has no intersection with the universal set (contains all elements of `α`). This situation can only occur when `s` is an empty set. Therefore, the theorem defines a characteristic property of an empty set in the context of a universal set. More concisely: A set is disjoint with the universal set if and only if it is the empty set.
`Set.Nonempty.to_subtype` theorem Set.Nonempty.to_subtype : ∀ {α : Type u} {s : Set α}, s.Nonempty → Nonempty ↑s The theorem `Set.Nonempty.to_subtype` states that for any type `α` and any set `s` of type `Set α`, if the set `s` is non-empty (expressed as `Set.Nonempty s`), then there exists an element in the subtype corresponding to `s` (expressed as `Nonempty ↑s`). In other words, if there exists an element in the original set, then there would also exist an element when we view the set as a subtype. More concisely: If `s : Set α` is non-empty, then there exists an element in the subtype `Nonempty ↑s`.
`Mathlib.Data.Set.Basic._auxLemma.57` theorem Mathlib.Data.Set.Basic._auxLemma.57 : ∀ {α : Type u} [inst : HasSubset α] {a b : α} [inst_1 : IsRefl α fun x x_1 => x ⊆ x_1] [inst_2 : IsAntisymm α fun x x_1 => x ⊆ x_1], (a = b) = (a ⊆ b ∧ b ⊆ a) This theorem states that for any type `α` that has a subset operation (`HasSubset α`) and is reflexive and antisymmetric with respect to this subset operation (`IsRefl α` and `IsAntisymm α`, respectively), two elements `a` and `b` of this type are equal if and only if `a` is a subset of `b` and `b` is a subset of `a`. In other words, in such a structure, two elements `a` and `b` are identical if they both include each other as subsets. More concisely: For any type `α` with `HasSubset α`, if `IsRefl α` and `IsAntisymm α` hold, then `a = b` if and only if `a ⊆ b` and `b ⊆ a`.
`Set.inter_diff_self` theorem Set.inter_diff_self : ∀ {α : Type u} (a b : Set α), a ∩ (b \ a) = ∅ This theorem states that for any type `α` and for any two sets `a` and `b` of type `α`, the intersection of set `a` and the difference of sets `b` and `a` is an empty set. In other words, the intersection of a set and the difference of another set and the former set always results in an empty set. In mathematical terms, if `a` and `b` are sets, then `a ∩ (b \ a) = ∅`. More concisely: The theorem asserts that for any type `α` and sets `a` and `b` of type `α`, the intersection of `a` and the set difference `(b \ a)` is the empty set. In symbols, `a ∩ (b \ a) = ∅`.
`Set.inter_assoc` theorem Set.inter_assoc : ∀ {α : Type u} (a b c : Set α), a ∩ b ∩ c = a ∩ (b ∩ c) This theorem states that for any given type `α` and any three sets `a`, `b`, and `c` of that type, the intersection of the three sets is associative. That is, the intersection of `a`, `b`, and `c` is the same whether we first intersect `a` and `b` and then intersect the result with `c`, or we first intersect `b` and `c` and then intersect the result with `a`. In mathematical terms, `a ∩ b ∩ c = a ∩ (b ∩ c)`. More concisely: For any type `α` and sets `a`, `b`, and `c` of that type, the intersection `a ∩ b ∩ c` is equal to `(a ∩ b) ∩ c`.
`Set.ite_empty_right` theorem Set.ite_empty_right : ∀ {α : Type u} (t s : Set α), t.ite s ∅ = s ∩ t The theorem `Set.ite_empty_right` states that for any type `α` and any two sets `t` and `s` of type `α`, the intersection of `s` with `t` is equal to the result of the `Set.ite` function with `t`, `s`, and the empty set as arguments. In other words, given any two sets `t` and `s`, the set obtained by taking the intersection of `s` with `t` and then adding the empty set after removing `t` (i.e., `Set.ite t s ∅`) is just the intersection of `s` and `t` (i.e., `s ∩ t`). More concisely: For any sets `s` and `t`, `s ∩ t` equals the result of applying `Set.ite` with arguments `t`, `s`, and the empty set.
`HasSSubset.SSubset.lt` theorem HasSSubset.SSubset.lt : ∀ {α : Type u} {s t : Set α}, s ⊂ t → s < t This theorem, referred to as an alias of the reverse direction of `Set.lt_iff_ssubset`, states that for any type `α` and any two sets `s` and `t` of type `α`, if `s` is a proper subset of `t` (denoted as `s ⊂ t`), then `s` is less than `t` (denoted as `s < t`). The 'less than' relation here is a metaphorical relation characterized by subset inclusion, meaning that all elements of `s` are in `t`, but `t` has at least one element which `s` does not have. More concisely: If `s ⊂ t` for sets `s` and `t` of type `α`, then `s < set.univ {x : α \| x ∈ t \ s}`.
`Set.ite_same` theorem Set.ite_same : ∀ {α : Type u} (t s : Set α), t.ite s s = s The theorem `Set.ite_same` states that for any type `α` and for any two sets `t` and `s` of type `α`, the operation `Set.ite` applied to `t`, `s`, and `s` (i.e., using the same set `s` for both the second and third arguments), returns `s` itself. In other words, this theorem states that if you take the intersection of a set `s` with another set `t`, and then form the union of the result with the difference of `s` and `t`, you get back the original set `s`. This is expressed mathematically as: `s ∩ t ∪ s \ t = s`. More concisely: The theorem `Set.ite_same` asserts that for any set `s` and `t`, `s ∩ t ∪ (s \ t) = s`.
`Set.diff_self_inter` theorem Set.diff_self_inter : ∀ {α : Type u} {s t : Set α}, s \ (s ∩ t) = s \ t This theorem states that for any type `α` and any two sets `s` and `t` of that type, the difference of `s` and the intersection of `s` and `t` is equal to the difference of `s` and `t`. In other words, removing the elements shared by `s` and `t` from `s` is equivalent to removing all the elements of `t` from `s`. This can be written in mathematical terms as $s \setminus (s \cap t) = s \setminus t$ for all sets `s` and `t` of elements of type `α`. More concisely: For all types `α` and sets `s` and `t` of type `α`, the set difference `s \ (s ∩ t)` equals `s \ t`.
`Set.union_diff_self` theorem Set.union_diff_self : ∀ {α : Type u} {s t : Set α}, s ∪ t \ s = s ∪ t This theorem, `Set.union_diff_self`, states that for any type `α` and for any two sets `s` and `t` of type `α`, the union of `s` and the difference of `t` and `s` is equal to the union of `s` and `t`. In other words, if you take a set `t`, remove all elements that `s` contains from it, and then take the union of this new set with `s`, you end up with the same set as if you had simply taken the union of `s` and `t` from the beginning. This theorem captures a fundamental property of set operations commonly used in set algebra. More concisely: For any type `α` and sets `s` and `t` of type `α`, `Set.union s (Set.diff t s) = Set.union s t`.
`Set.disjoint_iff` theorem Set.disjoint_iff : ∀ {α : Type u} {s t : Set α}, Disjoint s t ↔ s ∩ t ⊆ ∅ The theorem `Set.disjoint_iff` states that, for any type `α` and any two sets `s` and `t` of type `α`, `s` and `t` are disjoint if and only if the intersection of `s` and `t` is a subset of the empty set. In other words, two sets are defined as disjoint when their intersection contains no elements, which is equivalent to saying their intersection is contained within the empty set. More concisely: Two sets of type `α` are disjoint if and only if their intersection is equal to the empty set.
`Set.not_mem_empty` theorem Set.not_mem_empty : ∀ {α : Type u} (x : α), x ∉ ∅ This theorem states that for any type `α` and any element `x` of type `α`, `x` is not a member of the empty set. In other words, it formalizes the intuitive idea that the empty set, denoted by `∅`, contains no elements, regardless of the type of the elements we are considering. More concisely: The theorem asserts that for any type `α` and any element `x : α`, `x ∉ ∅`.
`Set.subset_union_left` theorem Set.subset_union_left : ∀ {α : Type u} (s t : Set α), s ⊆ s ∪ t The theorem `Set.subset_union_left` states that for any type `α` and any two sets `s` and `t` of type `α`, the set `s` is a subset of the union of `s` and `t`. This is a fundamental theorem in set theory which asserts that a set is always a subset of the union of itself with any other set. In terms of mathematical notation, this would be written as $s \subseteq s \cup t$ for all sets `s` and `t`. More concisely: For any sets `s` and `t`, `s` is a subset of their union, i.e., `s ⊆ s ∪ t`.
`Set.subset_diff_union` theorem Set.subset_diff_union : ∀ {α : Type u} (s t : Set α), s ⊆ s \ t ∪ t The theorem `Set.subset_diff_union` states that for any type `α` and for any two sets `s` and `t` of type `α`, `s` is a subset of the union of the difference of `s` and `t` and `t`. In other words, if we take away some elements from `s` to form a new set `s \ t`, and then form a union with `t`, the resulting set still contains `s` as a subset. In mathematical notation, for all sets `s` and `t`, `s` ⊆ `(s \ t) ∪ t`. More concisely: For all sets `s` and `t`, `s` is a subset of `(s \ t) ∪ t`.
`Set.inter_univ` theorem Set.inter_univ : ∀ {α : Type u} (a : Set α), a ∩ Set.univ = a The theorem `Set.inter_univ` states that for any type `α` and any set `a` of type `α`, the intersection of `a` with the universal set of type `α` (`Set.univ`) is equal to `a` itself. In more mathematical terms, given any set `a`, the intersection of `a` with the set of all elements (the universal set) always results in `a`. This is akin to the set theory concept that a set intersected with the universal set returns the original set. More concisely: For any set `a` of type `α`, `a ∩ Set.univ = a`.
`Set.Subset.rfl` theorem Set.Subset.rfl : ∀ {α : Type u} {s : Set α}, s ⊆ s This theorem, named `Set.Subset.rfl`, asserts that for any set `s` of a given type `α`, `s` is a subset of itself. In mathematical terms, for all sets `s`, we have `s ⊆ s`. This is a reflection of the reflexivity property of the subset relation in set theory. More concisely: For any set `s`, `s` is a subset of `s`. In mathematical notation, `s ⊆ s`.
`Set.nonempty_def` theorem Set.nonempty_def : ∀ {α : Type u} {s : Set α}, s.Nonempty ↔ ∃ x, x ∈ s The theorem `Set.nonempty_def` expresses the equivalence between the property `Set.Nonempty` of a set `s` of type `α` and the existence of an element in `s`. More specifically, it states that a set `s` is nonempty (`Set.Nonempty s`) if and only if there exists an element `x` such that `x` belongs to `s` (notated as `∃ x, x ∈ s`). This theorem serves to precisely define what it means for a set to be nonempty within the logic of Lean 4. More concisely: A set is nonempty if and only if it contains an element.
`Subsingleton.set_cases` theorem Subsingleton.set_cases : ∀ {α : Type u_1} [inst : Subsingleton α] {p : Set α → Prop}, p ∅ → p Set.univ → ∀ (s : Set α), p s This theorem, referred to as `Subsingleton.set_cases`, states that for any type `α` which is a Subsingleton (meaning it has at most one element), and for any property `p` applied to sets of `α`, if `p` holds for the empty set and `p` also holds for the universal set (the set containing all elements of `α`), then `p` must hold for any set of `α`. In essence, this theorem establishes that for Subsingleton types, any property that holds for the empty and universal sets must also hold for all sets of that type. More concisely: If `α` is a Subsingleton type and `p` is a property that holds for the empty set and the universal set of `α`, then `p` holds for every set of `α`.
`Disjoint.inter_eq` theorem Disjoint.inter_eq : ∀ {α : Type u} {s t : Set α}, Disjoint s t → s ∩ t = ∅ This theorem states that for any type `α` and any two sets `s` and `t` of type `α`, if the two sets are disjoint (i.e., their infimum is the bottom element of the given lattice), then the intersection of `s` and `t` is the empty set. In other words, if `s` and `t` have no elements in common (they are disjoint), then the set obtained by taking all the elements that belong to both `s` and `t` (the intersection of `s` and `t`) is an empty set. This is a formalization of the well-known mathematical fact about sets in set theory. More concisely: If two sets `s` and `t` of type `α` have no common elements (are disjoint), then their intersection `s ∩ t` is the empty set.
`Set.union_eq_right` theorem Set.union_eq_right : ∀ {α : Type u} {s t : Set α}, s ∪ t = t ↔ s ⊆ t This theorem states that for any type `α` and any two sets `s` and `t` of type `α`, the union of `s` and `t` is equal to `t` if and only if `s` is a subset of `t`. In terms of set theory, it is stating that a set `s` unioned with another set `t` results in the set `t` itself only when all elements of `s` are already in `t`, which is the definition of `s` being a subset of `t`. More concisely: For sets `s` and `t` of type `α`, `s ∪ t = t` if and only if `s ⊆ t`.
`Set.Subset.refl` theorem Set.Subset.refl : ∀ {α : Type u} (a : Set α), a ⊆ a This theorem states that, for any type `α` and any set `a` of type `α`, the set `a` is a subset of itself. In mathematical terms, this theorem establishes the reflexivity of the subset relation, i.e., for every set `a`, `a ⊆ a`. More concisely: For any set `a`, `a` is a subset of `a` (`a ⊆ a`).
`Set.diff_eq_empty` theorem Set.diff_eq_empty : ∀ {α : Type u} {s t : Set α}, s \ t = ∅ ↔ s ⊆ t The theorem `Set.diff_eq_empty` states that for any type `α` and any two sets `s` and `t` of type `α`, the set difference `s \ t` is the empty set if and only if `s` is a subset of `t`. In other words, if all elements of set `s` are also in set `t` (meaning `s` is a subset of `t`), then there are no elements in `s` that are not in `t`, hence the set difference `s \ t` is empty. Conversely, if the set difference `s \ t` is empty, that means there are no elements in `s` that are not also in `t`, so `s` must be a subset of `t`. More concisely: For any type α and sets s and t of type α, s \ t is the empty set if and only if s is a subset of t.
`Set.ite_inter_self` theorem Set.ite_inter_self : ∀ {α : Type u} (t s s' : Set α), t.ite s s' ∩ t = s ∩ t This theorem states that for any type `α` and any three sets `t`, `s`, and `s'` of type `α`, the intersection of the set defined by the "if-then-else" function `Set.ite` applied to `t`, `s`, and `s'` with the set `t` is equal to the intersection of the sets `s` and `t`. In mathematical terms, `Set.ite(t, s, s') ∩ t = s ∩ t`. This means that when we use the `Set.ite` function to create a set from `t`, `s`, and `s'`, any elements shared between that resultant set and `t` will also be shared between `s` and `t`. More concisely: For any type `α` and sets `t, s, s'` of type `α`, `Set.ite(t, s, s') �cap t = s ∩ t`.
`Subtype.mem` theorem Subtype.mem : ∀ {α : Type u_1} {s : Set α} (p : ↑s), ↑p ∈ s The theorem `Subtype.mem` states that for any type `α`, and any set `s` of type `α`, if we take an element `p` from the subtype induced by `s`, then `p` is indeed an element of the set `s`. Basically, this theorem is ensuring that the subtype construction correctly reflects the set membership relation. More concisely: Given a type `α` and a subset `s` of `α`, for any `p` in the subtype induced by `s`, we have `p ∈ s`.
`Mathlib.Data.Set.Basic._auxLemma.26` theorem Mathlib.Data.Set.Basic._auxLemma.26 : ∀ {α : Type u} (s t : Set α), (s ∩ t ⊆ s) = True This theorem states that for any type `α` and for any two sets `s` and `t` of type `α`, the intersection of `s` and `t` is always a subset of `s`. This is always true, as by definition, the intersection of two sets is the set of elements that both sets have in common, hence those elements are certainly part of set `s`. More concisely: For any type `α` and sets `s`, `t` of type `α`, `s ∩ t` is a subsets of `s`.
`MonotoneOn.inter` theorem MonotoneOn.inter : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder β] {f g : β → Set α} {s : Set β}, MonotoneOn f s → MonotoneOn g s → MonotoneOn (fun x => f x ∩ g x) s The theorem `MonotoneOn.inter` states that for any types `α` and `β` with a preorder defined on `β`, and for any functions `f` and `g` from `β` to the set of `α`, along with a set `s` of type `β`, if both `f` and `g` are monotone on `s`, then the function that maps `x` to the intersection of `f x` and `g x` is also monotone on `s`. In other words, the intersection of two monotone functions over a set in a preordered type is again a monotone function over that set. More concisely: If `f` and `g` are monotone functions from a preordered set `β` to type `α`, then their intersection `x ↦ f x ∩ g x` is also a monotone function on `β`.
`Mathlib.Data.Set.Basic._auxLemma.15` theorem Mathlib.Data.Set.Basic._auxLemma.15 : ∀ {α : Type u} (s : Set α), (s ⊆ Set.univ) = True The theorem `Mathlib.Data.Set.Basic._auxLemma.15` in Lean 4 states that for any type `α` and any set `s` of type `α`, the statement that `s` is a subset of the universal set `Set.univ` of type `α` is always true. This is an expression of the basic set-theoretic fact that every set is a subset of the universal set. More concisely: Every set is a subset of the universal set.
`Mathlib.Data.Set.Basic._auxLemma.45` theorem Mathlib.Data.Set.Basic._auxLemma.45 : ∀ {α : Sort u_1} {p : α → Prop} {b : Prop}, (∃ x, b ∧ p x) = (b ∧ ∃ x, p x) This theorem states that for any type `α`, any predicate `p` applied to `α`, and any proposition `b`, the existence of an element `x` such that both `b` and `p x` hold is equivalent to the conjunction `b` and the existence of an element `x` for which `p x` holds. In other words, the order of the conjunction and the existential quantifier does not matter in this context. More concisely: For any type `α`, predicate `p` on `α`, and proposition `b`, the existence of an `x` such that `p x` and `b` hold is equivalent to the existence of an `x` satisfying `p x` and `b` together.
`Set.inclusion_injective` theorem Set.inclusion_injective : ∀ {α : Type u_1} {s t : Set α} (h : s ⊆ t), Function.Injective (Set.inclusion h) := by sorry The theorem `Set.inclusion_injective` states that for any type `α` and for any two sets `s` and `t` of type `α`, if `s` is a subset of `t` (denoted as `s ⊆ t`), then the function `Set.inclusion h` is injective. In other words, `Set.inclusion h` maps distinct elements of `s` to distinct elements of `t`. Here, `Set.inclusion h` is a function that acts like the identity for elements in `s`, but each element is viewed as an element of `t` due to the subset relation. More concisely: If `s` is a subset of `t` in type `α`, then the function `Set.inclusion h` mapping elements of `s` to their respective elements in `t` is an injection.
`Set.Nonempty.some_mem` theorem Set.Nonempty.some_mem : ∀ {α : Type u} {s : Set α} (h : s.Nonempty), h.some ∈ s The theorem `Set.Nonempty.some_mem` states that for any type `α` and any set `s` of type `Set α`, if `s` is nonempty, then the element extracted by the function `Set.Nonempty.some` from the nonemptiness property `h` is an element of the set `s`. This theorem is significant because it allows us to extract an element from a nonempty set and guarantees that the extracted element is indeed a member of the set. More concisely: For any nonempty set `s` of type `α`, the element extracted by `Set.Nonempty.some` from its nonemptiness proof `h` is an element of `s`.
`Set.eq_of_mem_singleton` theorem Set.eq_of_mem_singleton : ∀ {α : Type u} {x y : α}, x ∈ {y} → x = y This theorem, `Set.eq_of_mem_singleton`, states that for any type 'α' and any elements 'x' and 'y' of that type, if 'x' is an element of the set that contains only 'y', then 'x' must be equal to 'y'. In other words, if 'x' is in a singleton set whose only element is 'y', 'x' must be identical to 'y'. This is a fundamental property of singleton sets in set theory. More concisely: For any type 'α' and elements 'x' and 'y' of that type, if 'x' is in the singleton set {y}, then 'x' equals 'y'.
`Set.nonempty_iff_ne_empty` theorem Set.nonempty_iff_ne_empty : ∀ {α : Type u} {s : Set α}, s.Nonempty ↔ s ≠ ∅ This theorem, `Set.nonempty_iff_ne_empty`, states that for any set `s` of type `α`, the assertion that the set `s` is nonempty is equivalent to the claim that the set `s` is not equal to the empty set. In other words, a set `s` is nonempty if and only if it is not an empty set. It's an assertion about the equivalence of two ways of expressing the notion of a set being nonempty: either directly using the `Set.Nonempty` predicate or by stating that the set is not the empty set. More concisely: A set is nonempty if and only if it is not equal to the empty set.
`Mathlib.Data.Set.Basic._auxLemma.12` theorem Mathlib.Data.Set.Basic._auxLemma.12 : ∀ {α : Type u}, ∅.Nonempty = False This theorem states that the empty set, denoted by ∅, is not nonempty for any type `α`. In other words, there does not exist an element `x` that belongs to the empty set ∅, regardless of the type of `x`. This is a fundamental property of the empty set in set theory. More concisely: The empty set is a subset of any type that has no elements.
`Set.mem_inter_iff` theorem Set.mem_inter_iff : ∀ {α : Type u} (x : α) (a b : Set α), x ∈ a ∩ b ↔ x ∈ a ∧ x ∈ b This theorem, `Set.mem_inter_iff`, states for any type `α`, an element `x` of that type, and any two sets `a` and `b` of that type, `x` belongs to the intersection of sets `a` and `b` if and only if `x` belongs to `a` and `x` belongs to `b`. In other words, membership in the intersection of two sets is equivalent to membership in both of the sets. More concisely: For any type `α` and sets `a` and `b` of type `α`, `x ∈ a ∧ x ∈ b` if and only if `x ∈ a ∩ b`.
`Set.Nonempty.ne_empty` theorem Set.Nonempty.ne_empty : ∀ {α : Type u} {s : Set α}, s.Nonempty → s ≠ ∅ This theorem, referred to as `Set.Nonempty.ne_empty`, states that for any type `α` and any set `s` of that type, if the set `s` is nonempty, then it must be unequal to the empty set. In other words, it establishes the forward direction of the equivalence between a set being nonempty and it not being the empty set. This theorem is particularly useful in proofs where the non-emptiness of a set directly implies certain properties or outcomes. More concisely: If a set is nonempty, then it is not equal to the empty set.
`Set.eq_empty_iff_forall_not_mem` theorem Set.eq_empty_iff_forall_not_mem : ∀ {α : Type u} {s : Set α}, s = ∅ ↔ ∀ (x : α), x ∉ s This theorem states that for any set `s` of a certain type `α`, the set `s` is equivalent to the empty set if and only if for every element `x` of type `α`, `x` is not a member of the set `s`. In other words, a set is empty if and only if no element of the type of the set belongs to the set. More concisely: A set of type `α` is empty if and only if it contains no elements of type `α`.
`Set.disjoint_right` theorem Set.disjoint_right : ∀ {α : Type u} {s t : Set α}, Disjoint s t ↔ ∀ ⦃a : α⦄, a ∈ t → a ∉ s This theorem states that for any type `α` and any sets `s` and `t` of type `α`, `s` and `t` are disjoint if and only if for all elements `a` in `t`, `a` is not in `s`. In other words, two sets are disjoint if there are no elements that are present in both sets, which is the classical definition of disjoint sets in set theory. In the context of this theorem, a set is defined as a collection of elements of a particular type that satisfy a certain property. More concisely: Two sets of the same type are disjoint if and only if none of their elements are common.
`Set.inter_left_comm` theorem Set.inter_left_comm : ∀ {α : Type u} (s₁ s₂ s₃ : Set α), s₁ ∩ (s₂ ∩ s₃) = s₂ ∩ (s₁ ∩ s₃) The theorem `Set.inter_left_comm` states that for any type `α` and any three sets of type `α`, namely `s₁`, `s₂`, and `s₃`, the intersection of `s₁` with the intersection of `s₂` and `s₃` is equal to the intersection of `s₂` with the intersection of `s₁` and `s₃`. This can be viewed as a form of the commutative property for set intersections, but with the intersection operation being applied to three sets, not just two. In other words, the order in which we take the intersection of three sets does not matter. More concisely: For any sets `s₁`, `s₂`, and `s₃` of type `α`, `s₁ ∩ (s₂ ∩ s₃) = s₂ ∩ (s₁ ∩ s₃)`.
`Set.disjoint_sdiff_right` theorem Set.disjoint_sdiff_right : ∀ {α : Type u} {s t : Set α}, Disjoint s (t \ s) This theorem states that for any type `α`, and any two sets `s` and `t` of this type, the set `s` and the difference set `t \ s` (i.e., the set of elements in `t` but not in `s`) are disjoint. "Disjoint" here is defined in the more general sense of lattice theory, which means that any element `x` that is less than or equal to both `s` and `t \ s` is also less than or equal to the bottom element of the lattice. More concisely: For any type `α` and sets `s` and `t` of this type, `s ∩ (t \ s) = ⊥`, where `∥` denotes the bottom element of the lattice.
`Mathlib.Data.Set.Basic._auxLemma.9` theorem Mathlib.Data.Set.Basic._auxLemma.9 : ∀ {α : Type u} (s : Set α), (∅ ⊆ s) = True This theorem states that for any set `s` of any type `α`, the empty set is a subset of `s`. In other words, this theorem confirms the general mathematical principle that the empty set is a subset of any given set. In mathematical notation, this would be represented as ∀s ∈ α, ∅ ⊆ s. More concisely: The empty set is a subset of any set. (Written mathematically as ∀α, ∅ ⊆ s, where α is the type of the set s and ∅ is the empty set.)
`Monotone.inter` theorem Monotone.inter : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder β] {f g : β → Set α}, Monotone f → Monotone g → Monotone fun x => f x ∩ g x The theorem `Monotone.inter` states that for any types `α` and `β`, and any preorder on `β`, if `f` and `g` are two functions from `β` to the set of `α`, and both `f` and `g` are monotone functions, then the function that maps each element `x` of `β` to the intersection of the sets `f(x)` and `g(x)` is also a monotone function. In simpler terms, if two functions are increasing, then the function that uses these two to create intersections of sets at each point is also increasing. More concisely: If `f` and `g` are monotonic functions from a preorder `β` to type `α`, then the function `x ∈β => f x ∩ g x` is also monotonic.
`Set.mem_of_eq_of_mem` theorem Set.mem_of_eq_of_mem : ∀ {α : Type u} {x y : α} {s : Set α}, x = y → y ∈ s → x ∈ s This theorem states that for any type `α`, any two elements `x` and `y` of that type, and any set `s` of elements of type `α`, if `x` equals `y` and `y` belongs to the set `s`, then `x` also belongs to the set `s`. In simpler terms, it says that if two elements are equal and one of them is in a set, then the other one is also in that set. This is consistent with the intuitive understanding of sets and equality. More concisely: If `x = y` and `y ∈ s`, then `x ∈ s`.
`Set.powerset_singleton` theorem Set.powerset_singleton : ∀ {α : Type u} (x : α), {x}.powerset = {∅, {x}} This theorem states that the powerset of a singleton set only contains the empty set and the singleton set itself. Given any type `α` and an element `x` of type `α`, the powerset of the set containing only `x` is equal to the set containing the empty set and the set containing `x`. In more mathematical terms, if we have a set `{x}` for some `x` in `α`, the powerset of this set, denoted P({x}), is `{∅, {x}}`. More concisely: The powerset of a singleton set is the set containing the empty set and the singleton set itself. In other words, P({x}) = {∅, {x}} for any `x` in `α`.
`Set.compl_inter` theorem Set.compl_inter : ∀ {α : Type u} (s t : Set α), (s ∩ t)ᶜ = sᶜ ∪ tᶜ This theorem states that for any two sets `s` and `t` of some type `α`, the complement of the intersection of `s` and `t` (denoted as `(s ∩ t)ᶜ`) is equal to the union of the complements of `s` and `t` (denoted as `sᶜ ∪ tᶜ`). This theorem is a formalization of one of the De Morgan's laws from set theory in Lean 4. More concisely: The complement of the intersection of sets `s` and `t` equals the union of their complements: `(s ∩ t)ᶜ = sᶜ ∪ tᶜ`.
`Set.inter_subset_inter_left` theorem Set.inter_subset_inter_left : ∀ {α : Type u} {s t : Set α} (u : Set α), s ⊆ t → s ∩ u ⊆ t ∩ u The theorem `Set.inter_subset_inter_left` states that for any type `α` and any three sets `s`, `t`, and `u` of type `α`, if set `s` is a subset of set `t` then the intersection of set `s` and set `u` is a subset of the intersection of set `t` and set `u`. In terms of set theory, this theorem tells us that if we have a subset relationship between two sets, then that relationship is preserved when we intersect both sets with a third one. More concisely: If `s` is a subset of `t`, then `s ∩ u` is a subset of `t ∩ u`.
`Set.mem_compl_singleton_iff` theorem Set.mem_compl_singleton_iff : ∀ {α : Type u} {a x : α}, x ∈ {a}ᶜ ↔ x ≠ a This theorem states that for any given type `α` and any two instances `a` and `x` of that type, `x` is a member of the complement of the singleton set `{a}` if and only if `x` is not equal to `a`. In other words, an element belongs to the complement of a singleton set if it is different from the single element in the original set. More concisely: For any type `α` and its elements `a` and `x`, `x ∈ ∉{a} ↔ x ≠ a`.
`Set.eq_univ_of_forall` theorem Set.eq_univ_of_forall : ∀ {α : Type u} {s : Set α}, (∀ (x : α), x ∈ s) → s = Set.univ This theorem states that for any set `s` of a type `α`, if every element `x` of type `α` belongs to `s` (i.e., `s` contains all elements of type `α`), then `s` is equal to the universal set of `α`, denoted by `Set.univ`. In other words, any set that contains all possible elements of a particular type is considered the universal set for that type. More concisely: If a set `s` of type `α` contains all elements of `α`, then `s` is equal to the universal set `Set.univ` of type `Set α`.
`Set.subset_inter_iff` theorem Set.subset_inter_iff : ∀ {α : Type u} {s t r : Set α}, r ⊆ s ∩ t ↔ r ⊆ s ∧ r ⊆ t This theorem, named `Set.subset_inter_iff`, says that for any type `α`, and any three sets `s`, `t`, and `r` of this type, `r` is a subset of the intersection of `s` and `t` if and only if `r` is a subset of `s` and `r` is a subset of `t`. In other words, a set is contained within two others simultaneously exactly when it is contained within their intersection. More concisely: For any type `α` and sets `s`, `t`, and `r` of type `α`, `r` is a subset of `s INTER t` if and only if `r` is a subset of both `s` and `t`.
`Mathlib.Data.Set.Basic._auxLemma.32` theorem Mathlib.Data.Set.Basic._auxLemma.32 : ∀ {α : Type u} {s t : Set α}, (t = s ∩ t) = (t ⊆ s) The theorem, named as `Mathlib.Data.Set.Basic._auxLemma.32`, states that for any type `α` and any two sets `s` and `t` of that type, the equality that `t` is the intersection of `s` and `t` is equivalent to saying that `t` is a subset of `s`. This captures the basic set theory idea that the intersection of a set with another set is a subset of the original set. More concisely: For any type α and sets s and t of that type, s intersect t = t if and only if t is a subset of s.
`Set.ssubset_insert` theorem Set.ssubset_insert : ∀ {α : Type u} {s : Set α} {a : α}, a ∉ s → s ⊂ insert a s This theorem states that for all types `α` and for any set `s` of type `α` and any element `a` of type `α`, if `a` is not a member of `s`, then `s` is a proper subset of the set resulting from inserting `a` into `s`. In other words, if you have a set and an element not in the set, adding the element to the set creates a set which is strictly larger than the original. More concisely: If `a` is not an element of set `s` of type `α`, then `insert a s` is a strictly larger set than `s`.
`Set.forall_insert_of_forall` theorem Set.forall_insert_of_forall : ∀ {α : Type u} {P : α → Prop} {a : α} {s : Set α}, (∀ x ∈ s, P x) → P a → ∀ x ∈ insert a s, P x This theorem states that for any type `α`, any property `P` of type `α → Prop`, any element `a` of type `α`, and any set `s` of type `Set α`, if every element `x` in `s` satisfies the property `P`, and the element `a` also satisfies `P`, then every element `x` in the set that results from inserting `a` into `s` also satisfies `P`. In other words, if all elements of a set and an additional element adhere to a certain property, then all elements of the updated set containing the additional element also adhere to the same property. More concisely: If `α` is a type, `P` is a property of type `α → Prop`, `a : α`, and `s : Set α` are such that `∀ x ∈ s, P x` and `P a`, then `P (mem s a)`. (This states that if every element of a set `s` has property `P` and `a` also has property `P`, then the inserted element `mem s a` also has property `P`.)
`Set.disjoint_empty` theorem Set.disjoint_empty : ∀ {α : Type u} (s : Set α), Disjoint s ∅ The theorem `Set.disjoint_empty` states that for all types `α` and for any set `s` of type `α`, the set `s` is disjoint with the empty set. In the context of this theorem, two sets are considered disjoint if their intersection (infimum) is the bottom element, which is the empty set in this case. More concisely: For all types α, the empty set is disjoint from any set s of type α. In other words, the intersection of s and the empty set is the empty set.
`Mathlib.Data.Set.Basic._auxLemma.84` theorem Mathlib.Data.Set.Basic._auxLemma.84 : ∀ {α : Type u} [inst : Nontrivial α] (x : α), {x}ᶜ.Nonempty = True := by sorry This theorem states that for any type `α` which is nontrivial (i.e., it contains at least two distinct elements), and for any element `x` of type `α`, the complement `{x}ᶜ` (set of all elements not equal to `x`) is nonempty. The theorem is always true regardless of the chosen `x` or nontrivial type `α`. In terms of mathematical language, it asserts that for every nontrivial set `α` and any element `x` in `α`, there exists at least one element in `α` that is not equal to `x`. More concisely: For any nontrivial type `α` and element `x` in `α`, the set of elements in `α` not equal to `x` is nonempty.
`Mathlib.Data.Set.Basic._auxLemma.14` theorem Mathlib.Data.Set.Basic._auxLemma.14 : ∀ {α : Type u}, (Set.univ = ∅) = IsEmpty α This theorem states that for any type `α`, the universal set of `α` is equal to the empty set if and only if `α` is an empty type. In other words, it establishes a correspondence between the condition of the universal set on `α` being empty and the type `α` having no instances. This is a foundation concept in type theory and set theory, connecting the properties of a type with the properties of the set of its instances. More concisely: The universal set of a type `α` is empty if and only if `α` is an empty type.
`Set.inclusion.proof_1` theorem Set.inclusion.proof_1 : ∀ {α : Type u_1} {s t : Set α}, s ⊆ t → ∀ (x : ↑s), ↑x ∈ t This theorem states that for any type `α`, and any two sets `s` and `t` of this type, if `s` is a subset of `t` (denoted `s ⊆ t`), then for any element `x` in the set `s` (denoted `x : ↑s`), this element `x` is also an element of the set `t` (denoted `↑x ∈ t`). In other words, if one set is a subset of another, then every element of the first set is also an element of the second set. More concisely: If `s ⊆ t` are sets, then for all `x : α`, if `x ∈ s`, then `x ∈ t`.
`Mathlib.Data.Set.Basic._auxLemma.3` theorem Mathlib.Data.Set.Basic._auxLemma.3 : ∀ {b a : Prop}, (∃ (_ : a), b) = (a ∧ b) This theorem, labelled as `Mathlib.Data.Set.Basic._auxLemma.3`, states that for any two propositions `a` and `b`, the existence of `b` under the assumption of `a` (notated as `∃ (_ : a), b`) is equivalent to the conjunction of `a` and `b` (notated as `a ∧ b`). In other words, if `b` holds true given `a`, then both `a` and `b` are true. More concisely: The theorem asserts that for all propositions `a` and `b`, `∃ (x : a), b` is logically equivalent to `a ∧ b`.
`Set.subset_singleton_iff_eq` theorem Set.subset_singleton_iff_eq : ∀ {α : Type u} {s : Set α} {x : α}, s ⊆ {x} ↔ s = ∅ ∨ s = {x} This theorem, named `Set.subset_singleton_iff_eq`, states that for any type `α`, any set `s` of type `α`, and any element `x` of type `α`, the subset relation `s ⊆ {x}` is true if and only if either `s` is the empty set `∅` or `s` is the singleton set `{x}`. In other words, a set `s` is a subset of a singleton set `{x}` if and only if `s` is either empty or it is a singleton set containing the same element as `{x}`. More concisely: A set `s` is a subset of the singleton set `{x}` if and only if `s` is empty or `s = {x}`.
`Set.subset_diff_singleton` theorem Set.subset_diff_singleton : ∀ {α : Type u} {x : α} {s t : Set α}, s ⊆ t → x ∉ s → s ⊆ t \ {x} The theorem `Set.subset_diff_singleton` states that for any type `α`, any element `x` of type `α`, and any sets `s` and `t` of the same type `α`, if `s` is a subset of `t` and `x` is not an element of `s`, then `s` is also a subset of the difference of `t` and the singleton set containing `x`. In other words, removing an element that is not in `s` from `t` does not affect the inclusion of `s` in `t`. More concisely: If `s` is a subset of `t` and `x ∉ s`, then `s` is a subset of `t \ {x}`.
`Set.nonempty_coe_sort` theorem Set.nonempty_coe_sort : ∀ {α : Type u} {s : Set α}, Nonempty ↑s ↔ s.Nonempty This theorem, `Set.nonempty_coe_sort`, states that for any type `α` and any set `s` of type `α`, the property `Nonempty ↑s` (i.e., the set `s` has a `Nonempty` type when converted to another type using an explicit or implicit coercion function) is equivalent to `Set.Nonempty s` (i.e., the set `s` is not empty). In other words, a set `s` is not empty if and only if it remains nonempty after type coercion. More concisely: The theorem asserts that for any set `s` of type `α`, the set `s` is nonempty if and only if its coerced version `Nonempty ↑s` has type `Nonempty α`.
`Set.insert_subset` theorem Set.insert_subset : ∀ {α : Type u} {a : α} {s t : Set α}, a ∈ t → s ⊆ t → insert a s ⊆ t The theorem `Set.insert_subset` states that for any type `α`, any element `a` of type `α`, and any sets `s` and `t` of type `α`, if `a` belongs to set `t` and set `s` is a subset of `t`, then the set resulting from inserting `a` into `s` is also a subset of `t`. In other words, it ensures that adding an element to a subset, where the element is already part of the superset, will result in another subset of that superset. More concisely: If `a` is an element of set `t` and `s` is a subset of `t`, then `a :: s` (the set obtained by inserting `a` into `s`) is a subset of `t`.
`Set.insert_diff_singleton` theorem Set.insert_diff_singleton : ∀ {α : Type u} {a : α} {s : Set α}, insert a (s \ {a}) = insert a s This theorem states that for any type `α`, any element `a` of that type, and any set `s` of elements of that type, the set obtained by inserting `a` into the difference between `s` and the singleton set containing `a` is the same as the set obtained by simply inserting `a` into `s`. In other words, if you remove `a` from `s` and then add it back, you end up with the same set as if you just added `a` to `s`, even if `a` was already in `s`. This is expressed mathematically as ∀ {α : Type u} {a : α} {s : Set α}, insert a (s \ {a}) = insert a s. More concisely: For any type `α`, set `s` of elements, and element `a` in `α`, adding `a` to the set difference `s \ {a}` yields the same result as simply adding `a` to `s`. In mathematical notation: `insert a (s \ {a}) = insert a s`.
`Set.subset_compl_singleton_iff` theorem Set.subset_compl_singleton_iff : ∀ {α : Type u} {a : α} {s : Set α}, s ⊆ {a}ᶜ ↔ a ∉ s This theorem, named `Set.subset_compl_singleton_iff`, is a universal statement in the context of set theory. It asserts that for any type `α`, any element `a` of this type, and any set `s` of elements of type `α`, the set `s` is a subset of the complement of the singleton set `{a}` if and only if the element `a` is not an element of the set `s`. In mathematical terms, we can say that $s \subseteq (\{a\})^c$ if and only if $a \notin s$. More concisely: For any set $s$ and element $a$ in type $\alpha$, $s \subseteq \{a\}^c$ if and only if $a \notin s$.
`Set.insert_diff_singleton_comm` theorem Set.insert_diff_singleton_comm : ∀ {α : Type u} {a b : α}, a ≠ b → ∀ (s : Set α), insert a (s \ {b}) = insert a s \ {b} The theorem `Set.insert_diff_singleton_comm` states that for any type `α`, and any two elements `a` and `b` of that type such that `a` and `b` are not equal, and for any set `s` of type `α`, inserting `a` into the set difference of `s` and the singleton set containing `b` is the same as the set difference of inserting `a` into `s` and the singleton set containing `b`. In other words, the insertion of `a` and the removal of `b` commute with each other in any set `s`. More concisely: For any type `α` and elements `a ≠ b` of `α`, and sets `s : α`, `Set.insert a (s \ {b}) = (s \ {b}) \ {a}`.
`Set.inter_compl_self` theorem Set.inter_compl_self : ∀ {α : Type u} (s : Set α), s ∩ sᶜ = ∅ This theorem states that for all types `α` and any set `s` of type `α`, the intersection of the set `s` and its complement `sᶜ` is always an empty set. In other words, there are no elements that can be found both in a set and its complement, which aligns with the mathematical concept where a set and its complement are disjoint and their intersection is the empty set. More concisely: For all types `α` and sets `s` of type `α` in Lean 4, the intersection of `s` and its complement `sᶜ` is an empty set. `∥s∥ = ∥sᶜ∥ → s ∩ sᶜ = ∅`.
`Set.insert_inter_of_mem` theorem Set.insert_inter_of_mem : ∀ {α : Type u} {a : α} {s t : Set α}, a ∈ t → insert a s ∩ t = insert a (s ∩ t) := by sorry This theorem, named `Set.insert_inter_of_mem`, states that for any type `α`, any element `a` of type `α`, and any two sets `s` and `t` of type `α`, if element `a` belongs to set `t`, then the intersection of the set obtained by inserting `a` into `s` and set `t` is equal to the set obtained by inserting `a` into the intersection of sets `s` and `t`. In other words, if `a` is in `t`, then adding `a` to `s` before or after intersecting `s` and `t` doesn't affect the resultant set. More concisely: For any type `α`, sets `s` and `t` of type `α`, and element `a` of type `α` in `t`, the set `(a :: s) ∩ t` equals `a :: (s ∩ t)`.
`Set.mem_of_mem_inter_right` theorem Set.mem_of_mem_inter_right : ∀ {α : Type u} {x : α} {a b : Set α}, x ∈ a ∩ b → x ∈ b The theorem `Set.mem_of_mem_inter_right` states that for any type `α`, any element `x` of type `α`, and any two sets `a` and `b` of type `α`, if `x` belongs to the intersection of `a` and `b`, then `x` belongs to `b`. In other words, given any object and two sets, if the object is a member of both sets (i.e., in the intersection of the sets), then it is a member of the second set. More concisely: For any type `α` and sets `a` and `b` of type `α`, if `x` is an element of `a` and `a ∩ b`, then `x` belongs to `b`.
`Set.mem_singleton_iff` theorem Set.mem_singleton_iff : ∀ {α : Type u} {a b : α}, a ∈ {b} ↔ a = b This theorem states that for any type `α` and any two elements `a` and `b` of that type, `a` belongs to the singleton set `{b}` if and only if `a` is equal to `b`. In other words, an element `a` is a member of a set that only contains `b` if `a` and `b` are actually the same element. More concisely: For any type `α` and elements `a, b : α`, `a ∈ {b} ↔ a = b`.
`Set.singleton_nonempty` theorem Set.singleton_nonempty : ∀ {α : Type u} (a : α), {a}.Nonempty The theorem `Set.singleton_nonempty` states that for any type `α` and for any element `a` of type `α`, the singleton set containing `a` is not empty. In other words, it asserts that a set that contains at least one element is indeed nonempty. This serves as a fundamental property of singleton sets in the universe of sets in the type theory. More concisely: For any type `α` and element `a` of type `α`, the singleton set `{a : α}` is a nonempty set.
`Set.monotone_powerset` theorem Set.monotone_powerset : ∀ {α : Type u}, Monotone Set.powerset The theorem `Set.monotone_powerset` states that for all types `α`, the powerset function is monotone. In other words, for any two sets `a` and `b` of type `α`, if `a` is a subset of `b` (`a ≤ b`), then the powerset of `a` is a subset of the powerset of `b` (`Set.powerset a ≤ Set.powerset b`). The powerset of a set is the set of all its subsets. More concisely: For any type `α`, the powerset function is monotone, that is, for all sets `a` and `b` of type `α`, if `a` is a subset of `b`, then `Set.powerset a` is a subset of `Set.powerset b`.
`Set.Nonempty.coe_sort` theorem Set.Nonempty.coe_sort : ∀ {α : Type u} {s : Set α}, s.Nonempty → Nonempty ↑s This theorem, referred to as an alias of the reverse direction of `Set.nonempty_coe_sort`, states that for any type `α` and any set `s` of type `α`, if the set `s` is nonempty, then there exists an element in the type-casted set `s` (denoted by `↑s`). In other words, if a set `s` has at least one element, then the type-casted version of the set also contains at least one element. More concisely: If `s` is a nonempty set of type `α`, then `↑s` contains an element.
`Set.eq_empty_of_subset_empty` theorem Set.eq_empty_of_subset_empty : ∀ {α : Type u} {s : Set α}, s ⊆ ∅ → s = ∅ This theorem states that for any set `s` of type `α`, if `s` is a subset of the empty set `∅`, then `s` must be the empty set. In other words, the only set that can be a subset of the empty set is the empty set itself. This is in line with the mathematical principle that the empty set is a subset of every set, including itself. More concisely: If a set `s` is a subset of the empty set `∅`, then `s` is the empty set.
`Set.sep_univ` theorem Set.sep_univ : ∀ {α : Type u} {p : α → Prop}, {x \| x ∈ Set.univ ∧ p x} = {x \| p x} This theorem states that for any type `α` and any property `p` that elements of `α` may or may not satisfy, the set of elements in `α` that satisfy both the condition of being in the universal set and the property `p` is equal to the set of elements in `α` that satisfy the property `p` alone. In other words, restricting the universe with the universal set on a type `α` (which contains all elements of `α`) has no effect when further narrowing down the elements of `α` with property `p`. The universal set here acts as an identity element for set restriction in this context. More concisely: For any type `α` and property `p`, the set of elements in `α` that satisfy both the universal condition and property `p` equals the set of elements in `α` that satisfy property `p`.
`Mathlib.Data.Set.Basic._auxLemma.8` theorem Mathlib.Data.Set.Basic._auxLemma.8 : ∀ {α : Type u} (x : α), (x ∈ ∅) = False This theorem, `Mathlib.Data.Set.Basic._auxLemma.8`, states that for any type `α` and an element `x` of this type, the proposition that `x` is an element of the empty set is always False. In other words, no element can belong to the empty set, irrespective of its type. More concisely: The theorem asserts that for all types α and elements x of α, x is not an element of the empty set.
`Mathlib.Data.Set.Basic._auxLemma.22` theorem Mathlib.Data.Set.Basic._auxLemma.22 : ∀ {α : Type u} {s t u : Set α}, (s ∪ t ⊆ u) = (s ⊆ u ∧ t ⊆ u) The theorem states that for any type `α` and any three sets `s`, `t`, and `u` of type `α`, the union of `s` and `t` is a subset of `u` if and only if both `s` and `t` are subsets of `u`. In other words, all elements of `s` and `t` are in `u` if and only if every element of `s` is in `u` and every element of `t` is in `u`. This theorem captures a fundamental property of set theory. More concisely: For any set `α` and sets `s`, `t`, and `u` of type `α`, `s ∪ t ⊆ u` if and only if `s ⊆ u` and `t ⊆ u`.
`Set.not_nonempty_iff_eq_empty'` theorem Set.not_nonempty_iff_eq_empty' : ∀ {α : Type u} {s : Set α}, ¬Nonempty ↑s ↔ s = ∅ This theorem states that for any type `α` and any set `s` of type `α`, the set `s` is not nonempty if and only if the set `s` is equal to the empty set. In other words, it states that a set `s` has no elements (`¬Nonempty ↑s`) if and only if `s` is the same as the empty set (`s = ∅`). More concisely: A set `s` of type `α` is empty if and only if `s` has no elements, that is, `∅ = s <-> ∀x, x ∉ s`.
`Set.mem_union_left` theorem Set.mem_union_left : ∀ {α : Type u} {x : α} {a : Set α} (b : Set α), x ∈ a → x ∈ a ∪ b The theorem `Set.mem_union_left` states that for any type `α`, any element `x` of type `α`, and any two sets `a` and `b` of type `α`, if `x` is a member of set `a`, then `x` is also a member of the union of sets `a` and `b`. This is a fundamental property of set theory, represented in Lean 4. The symbol `∪` represents the union operation in set theory. More concisely: For any type `α`, if `x` is an element of set `a` and `a` is a subset of `a ∪ b`, then `x` is an element of `b ∪ a`. (This is the converse statement of `Set.mem_union_left` in Lean 4.)
`Disjoint.subset_compl_right` theorem Disjoint.subset_compl_right : ∀ {α : Type u} {s t : Set α}, Disjoint s t → s ⊆ tᶜ This theorem, named `Disjoint.subset_compl_right`, states that for any type `α` and any two sets `s` and `t` of type `α`, if `s` and `t` are disjoint, then `s` is a subset of the complement of `t`. In other words, if no element from `s` is found in `t`, then all elements of `s` must be outside of `t`, i.e., in `t`'s complement. The notion of disjointness here generalizes the concept of disjoint sets to any two elements of a lattice where their infimum (greatest lower bound) is the bottom element. More concisely: If sets `s` and `t` are disjoint in a lattice, then `s` is a subset of the complement of `t`.
`Set.inter_eq_self_of_subset_left` theorem Set.inter_eq_self_of_subset_left : ∀ {α : Type u} {s t : Set α}, s ⊆ t → s ∩ t = s This theorem states that for any type `α` and any sets `s` and `t` of this type, if `s` is a subset of `t`, then the intersection of `s` and `t` is equal to `s`. In other words, all elements in `s` are also in `t`, so the common elements between `s` and `t` are just the elements of `s`. This can be expressed in mathematical notation as: if $s \subseteq t$, then $s \cap t = s$. More concisely: For any sets `s` and `t` of type `α`, if `s` is a subset of `t`, then `s` is equal to their intersection, i.e., `s = s ∩ t`.
`Set.union_self` theorem Set.union_self : ∀ {α : Type u} (a : Set α), a ∪ a = a The theorem `Set.union_self` states that for any type `α` and any set `a` of that type, the union of `a` with itself is equal to `a`. In other words, for any element in some category, combining it with itself does not create a new, distinct collection. This mirrors the mathematical property of union in set theory, where the union of a set with itself is just the set itself. The symbol `∪` is used to represent union in this context. More concisely: For any set `a` of type `α`, `a ∪ a = a`.
`Mathlib.Data.Set.Basic._auxLemma.77` theorem Mathlib.Data.Set.Basic._auxLemma.77 : ∀ {α : Type u} {s t : Set α}, Disjoint s t = (s ∩ t ⊆ ∅) The theorem `Mathlib.Data.Set.Basic._auxLemma.77` states that for any type `α` and for all sets `s` and `t` of this type, `s` and `t` are disjoint if and only if the intersection of `s` and `t` is a subset of the empty set. In other words, two sets are defined as disjoint when their intersection contains no elements. More concisely: Two sets of type `α` are disjoint if and only if their intersection is a subset of the empty set.
`Set.disjoint_singleton_left` theorem Set.disjoint_singleton_left : ∀ {α : Type u} {a : α} {s : Set α}, Disjoint {a} s ↔ a ∉ s The theorem `Set.disjoint_singleton_left` states that for any type `α`, any element `a` of that type, and any set `s` of type `α`, the singleton set containing `a` is disjoint with `s` if and only if `a` is not an element of `s`. In other words, a singleton set and another set are disjoint if the single element of the singleton set does not belong to the other set. Here, disjointness is defined in the sense of lattice theory, i.e., two elements of a lattice are considered disjoint if their infimum (greatest lower bound) is the bottom element of the lattice. More concisely: For any type α, set s of α, and element a of α, the singleton set {a} is disjoint with s if and only if a ∉ s.
`Set.union_subset_union_right` theorem Set.union_subset_union_right : ∀ {α : Type u} (s : Set α) {t₁ t₂ : Set α}, t₁ ⊆ t₂ → s ∪ t₁ ⊆ s ∪ t₂ The theorem `Set.union_subset_union_right` states that for any type `α` and any set `s` of type `α`, if set `t₁` is a subset of set `t₂`, then the union of `s` and `t₁` is also a subset of the union of `s` and `t₂`. In other words, if we have a third set `t₁` that is a subset of another set `t₂`, increasing the set `s` by adding `t₁` won't make it larger than what we would get if we added `t₂` instead. This is a formalization of a basic principle of set theory. More concisely: For any sets `s` and `t₁` such that `t₁` is a subset of `t₂`, we have `s ∪ t₁ ⊆ s ∪ t₂`.
`Set.diff_compl` theorem Set.diff_compl : ∀ {α : Type u} {s t : Set α}, s \ tᶜ = s ∩ t The theorem `Set.diff_compl` states that for any type `α` and any two sets `s` and `t` of type `α`, the difference of set `s` and the complement of set `t` is equal to the intersection of `s` and `t`. In mathematical terms, this could be written as $s \setminus t^c = s \cap t$. Essentially, this theorem is stating a fundamental property of set operations in relation to complements and intersections. More concisely: The theorem `Set.diff_compl` asserts that for any type `α` and sets `s` and `t` of type `α`, their set difference `s \ t` equals their intersection `s ∩ t` and the complement of `t`, `t^c`, respectively, `s \ (t^c) = s ∩ t`.
`Set.diff_diff_cancel_left` theorem Set.diff_diff_cancel_left : ∀ {α : Type u} {s t : Set α}, s ⊆ t → t \ (t \ s) = s This theorem states that for any type `α` and for any two sets `s` and `t` of this type, if `s` is a subset of `t`, then the set difference of `t` and the set difference of `t` and `s` is equal to `s`. In other words, if you take all elements in `t` not in `s` and then remove these from `t`, you are left with `s`. This result holds for any type and is fundamental in set theory. This is often written in mathematical notation as: if $s \subseteq t$, then $(t \ (t \ s)) = s$. More concisely: For any type `α` and sets `s` and `t` of type `α`, if `s` is a subset of `t`, then `t \ (t \ s) = s`.
`Mathlib.Data.Set.Basic._auxLemma.80` theorem Mathlib.Data.Set.Basic._auxLemma.80 : ∀ {α : Type u} {s t : Set α}, (s ⊂ t) = ∃ a ∉ s, insert a s ⊆ t := by sorry This theorem states that for any type `α` and any two sets `s` and `t` of type `α`, the proposition that `s` is a proper subset of `t` is equivalent to the existence of an element `a` of type `α` that is not in `s` but when added to `s`, the resulting set is a subset of `t`. In mathematical terms, we say that "$s$ is a proper subset of $t$" if and only if there exists an element $a$ such that $a$ is not an element of $s$ and the set $s$ union with $\{a\}$ is a subset of $t$. More concisely: A set `s` is a proper subset of set `t` if and only if there exists an element `a` not in `s` such that `s ∪ {a} ⊆ t`.
`Set.diff_singleton_subset_iff` theorem Set.diff_singleton_subset_iff : ∀ {α : Type u} {x : α} {s t : Set α}, s \ {x} ⊆ t ↔ s ⊆ insert x t This theorem states that for any type `α`, any element `x` of that type, and any two sets `s` and `t` of that type, the set `s` without the element `x` is a subset of `t` if and only if the set `s` is a subset of the set `t` with `x` inserted. In mathematical terms, given `s \ {x} ⊆ t`, it implies `s ⊆ insert x t`, and vice versa. That is, removing an element from one set and testing for subset inclusion is equivalent to inserting that element into the other set and testing for subset inclusion. More concisely: For any type `α`, sets `s` and `t` of that type, and element `x` of `α`, we have `s \ {x} ⊆ t` if and only if `s ⊆ insert x t`.
`Mathlib.Data.Set.Basic._auxLemma.2` theorem Mathlib.Data.Set.Basic._auxLemma.2 : ∀ {α : Sort u_1} {p : α → Prop}, (¬∀ (x : α), p x) = ∃ x, ¬p x This theorem, `Mathlib.Data.Set.Basic._auxLemma.2`, states that for any type `α` and any predicate `p` that applies to `α`, the statement "it is not the case that every element of `α` satisfies `p`" is equivalent to "there exists an element of `α` that does not satisfy `p`". It presents a foundational concept in formal logic, expressing the negation of a universal quantifier as an existential quantifier with a negated predicate. More concisely: The theorem `Mathlib.Data.Set.Basic._auxLemma.2` in Lean 4 states that the negation of "every element of type `α` satisfies predicate `p`" is equivalent to "there exists an element in `α` that does not satisfy `p`."
`Set.le_iff_subset` theorem Set.le_iff_subset : ∀ {α : Type u} {s t : Set α}, s ≤ t ↔ s ⊆ t This theorem states that for any given type `α` and any two sets `s` and `t` of this type, `s` is less than or equal to `t` if and only if `s` is a subset of `t`. In the context of set theory, the "less than or equal to" relation becomes the subset relation. This means that every element of set `s` is also an element of set `t`. More concisely: For any type `α`, sets `s` and `t` of type `α`, the relation `s ⊆ t` holds if and only if `s ≤ t` holds. (In the context of set theory, `s ≤ t` denotes `s` is a subset of `t`. )
`Set.subset_compl_iff_disjoint_right` theorem Set.subset_compl_iff_disjoint_right : ∀ {α : Type u} {s t : Set α}, s ⊆ tᶜ ↔ Disjoint s t The theorem `Set.subset_compl_iff_disjoint_right` states that for any type `α` and any sets `s` and `t` of type `α`, the set `s` is a subset of the complement of `t` if and only if the sets `s` and `t` are disjoint. In other words, no element in `s` also belongs to `t` if and only if all elements in `s` belong to the complement of `t`. The term "disjoint" here refers to the generalization of disjoint sets in a lattice context, meaning that the infimum (greatest lower bound) of the two sets is the bottom element of the lattice. More concisely: For sets $s$ and $t$ in type $\alpha$, $s \subseteq \neg t$ if and only if $s \cap t = \bot$, where $\neg$ denotes the complement and $\bot$ the bottom element of the lattice.
`Set.empty_subset` theorem Set.empty_subset : ∀ {α : Type u} (s : Set α), ∅ ⊆ s This theorem states that for any set `s` of a type `α`, the empty set is a subset of `s`. In mathematical terms, for every set `s` in the universe of discourse, it always holds that the empty set is a subset of `s`. This is a fundamental property of set theory, as the empty set contains no elements and therefore cannot contain any elements not in `s`. More concisely: For any set `s`, the empty set is a subset of `s`.
`Set.subset_insert` theorem Set.subset_insert : ∀ {α : Type u} (x : α) (s : Set α), s ⊆ insert x s This theorem, `Set.subset_insert`, states that for all types `α`, given an element `x` of type `α` and a set `s` of elements of type `α`, `s` is a subset of the set obtained by inserting `x` into `s`. Here, the `insert x s` operation represents the set which contains all elements from `s` as well as `x` (if not already present in `s`). The symbol `⊆` denotes the subset relation, which means that all elements of `s` are also elements of the set `insert x s`. More concisely: For all types `α` and sets `s` of elements of type `α`, and all `x` in `α`, the set `s` is a subset of the set `insert x s`.
`Set.subset_inter` theorem Set.subset_inter : ∀ {α : Type u} {s t r : Set α}, r ⊆ s → r ⊆ t → r ⊆ s ∩ t The theorem `Set.subset_inter` states that for all types `α` and for all sets `s`, `t`, and `r` of type `α`, if `r` is a subset of both `s` and `t`, then `r` is a subset of the intersection of `s` and `t`. In other words, if every element of `r` is also an element of `s` and `t`, then every element of `r` is also an element of the intersection of `s` and `t`. This is a fundamental property of set intersection in the context of set theory. More concisely: If sets `r`, `s`, and `t` have the property that `r` is a subset of both `s` and `t`, then `r` is a subset of `s ∩ t`.
`Set.singleton_eq_singleton_iff` theorem Set.singleton_eq_singleton_iff : ∀ {α : Type u} {x y : α}, {x} = {y} ↔ x = y This theorem states that for all types `α` and for any two elements `x` and `y` of that type, the set containing only `x` is equal to the set containing only `y` if and only if `x` is equal to `y`. In other words, two singleton sets (sets with only one element) are equal if and only if their elements are equal. More concisely: For any type `α` and elements `x, y` of type `α`, the singletons `{x}` and `{y}` are equal if and only if `x = y`.
`Set.powerset_univ` theorem Set.powerset_univ : ∀ {α : Type u}, Set.univ.powerset = Set.univ The theorem `Set.powerset_univ` states that for any type `α`, the powerset of the universal set of `α` is equal to the universal set itself. In terms of set theory, this can be understood as saying that the collection of all possible subsets of a given set (which is the universal set of `α` in this context), is as large as the universal set itself. Here, `𝒫 Set.univ` represents the powerset of the universal set, in other words, the set of all subsets of the universal set. More concisely: For any type `α`, the powerset of its universal set is equal to the universal set itself. In set theory, this is expressed as `𝒫 Set.univ = Set.univ`.
`Mathlib.Data.Set.Basic._auxLemma.17` theorem Mathlib.Data.Set.Basic._auxLemma.17 : ∀ {α : Type u} (x : α) (a b : Set α), (x ∈ a ∪ b) = (x ∈ a ∨ x ∈ b) := by sorry This theorem is about the union of two sets in set theory. Given a type `α`, and three elements: `x`, which is of type `α`, and `a` and `b` which are sets of type `α`, it states that the membership of `x` in the union of sets `a` and `b` is equivalent to saying that `x` is a member of set `a` or `x` is a member of set `b`. This is a fundamental property of set unions in mathematics, often denoted as `x ∈ a ∪ b` is equivalent to `x ∈ a ∨ x ∈ b`. More concisely: For any type `α` and sets `a` and `b` of type `α`, the element `x` belongs to the union `a ∪ b` if and only if `x` belongs to `a` or `x` belongs to `b`.
`Set.mem_of_mem_of_subset` theorem Set.mem_of_mem_of_subset : ∀ {α : Type u} {x : α} {s t : Set α}, x ∈ s → s ⊆ t → x ∈ t The theorem `Set.mem_of_mem_of_subset` states that for any type α and any elements x of type α and sets s and t of type α, if x is a member of set s and set s is a subset of set t, then x is also a member of set t. This encapsulates the intuitive idea that if an item belongs to a smaller group (subset) and that smaller group is part of a larger group (superset), then the item also belongs to the larger group. More concisely: If `s` is a subset of `t` and `x` is an element of `s`, then `x` is an element of `t`.
`Set.union_inter_cancel_right` theorem Set.union_inter_cancel_right : ∀ {α : Type u} {s t : Set α}, (s ∪ t) ∩ t = t The theorem `Set.union_inter_cancel_right` states that for any type `α` and any sets `s` and `t` of type `α`, the intersection of the union of `s` and `t` with `t` is equal to `t`. This corresponds to the principle in set theory which asserts that when you unite a set `t` with another set `s` and then intersect it with `t`, you get back the set `t`. This is expressed mathematically as $(s \cup t) \cap t = t$. More concisely: For any type `α` and sets `s` and `t` of type `α`, `(s ∪ t) ∩ t = t`.
`Set.mem_insert_of_mem` theorem Set.mem_insert_of_mem : ∀ {α : Type u} {x : α} {s : Set α} (y : α), x ∈ s → x ∈ insert y s The theorem `Set.mem_insert_of_mem` states that for any type `α`, any element `x` of type `α`, and any set `s` of type `Set α`, if `x` is an element of `s`, then `x` is also an element of the set obtained by inserting any element `y` of type `α` into `s`. In other words, if `x` belongs to a set `s`, then `x` will still belong to the set after we add another element to `s`. More concisely: If `x` is an element of set `s` and `y` is any element, then `x` is an element of the set obtained by inserting `y` into `s` (i.e., `s.insert y`).
`Set.union_empty` theorem Set.union_empty : ∀ {α : Type u} (a : Set α), a ∪ ∅ = a This theorem states that for any set `a` of any type `α`, the union of `a` with the empty set is equal to `a` itself. In other words, adding an empty set to any other set doesn't change the original set. In mathematical terms, if `α` is any type and `a` is a set of type `α`, then `a ∪ ∅ = a`. More concisely: For any set `a` of type `α`, the union of `a` with the empty set `∅` equals `a`: `a ∪ ∅ = a`.
`Set.subset_compl_iff_disjoint_left` theorem Set.subset_compl_iff_disjoint_left : ∀ {α : Type u} {s t : Set α}, s ⊆ tᶜ ↔ Disjoint t s This theorem states that for any type `α` and any sets `s` and `t` of type `α`, `s` is a subset of the complement of `t` if and only if `t` and `s` are disjoint. In other words, all elements of `s` are not in `t` if and only if there's no element that belongs to both `t` and `s`. This theorem provides a connection between the concepts of set complement and disjointness in the context of set theory. More concisely: For sets `s` and `t` of type `α`, `s` is a subset of the complement of `t` if and only if `s` and `t` are disjoint.
`Set.disjoint_of_subset_left` theorem Set.disjoint_of_subset_left : ∀ {α : Type u} {s t u : Set α}, s ⊆ u → Disjoint u t → Disjoint s t The theorem `Set.disjoint_of_subset_left` states that for any type `α` and any sets `s`, `t`, and `u` of that type, if `s` is a subset of `u` and `u` is disjoint from `t`, then `s` is also disjoint from `t`. In other words, if all elements of `s` are also elements of `u` and no element of `u` can be an element of `t`, then no element of `s` can be an element of `t`. This theorem generalizes the intuitive notion of disjoint sets, and is relevant in the context of partial orders and lattice theory. More concisely: If a subset `s` of type `α` is contained in another set `u` and `u` is disjoint from set `t`, then `s` is disjoint from `t`.
`Set.disjoint_singleton` theorem Set.disjoint_singleton : ∀ {α : Type u} {a b : α}, Disjoint {a} {b} ↔ a ≠ b This theorem states that for any type `α` and any two elements `a` and `b` of type `α`, the singleton sets `{a}` and `{b}` are disjoint (in the sense that their infimum is the bottom element) if and only if `a` is not equal to `b`. In other words, two single-element sets are disjoint according to our definition if the elements they contain are distinct. More concisely: For any type `α` and elements `a` and `b` of type `α`, the singleton sets `{a}` and `{b}` have empty intersection, i.e., their infimum is the bottom element, if and only if `a` is not equal to `b`.
`SetCoe.ext` theorem SetCoe.ext : ∀ {α : Type u} {s : Set α} {a b : ↑s}, ↑a = ↑b → a = b The theorem `SetCoe.ext` states that for any type `α` and any set `s` of type `α`, given any two elements `a` and `b` of the subtype corresponding to `s`, if the elements `a` and `b`, when considered as elements of the original type `α` (by applying the coercion function `↑`), are equal, then `a` and `b` themselves (considered as elements of the subtype) are also equal. This essentially says that equality within the original type implies equality within the subtype. More concisely: If `α` is a type and `s : Set α` is a subset, then for all `a, b ∈ s`, `a = b` in `α` implies `a = b` in `s`.
`Set.compl_empty` theorem Set.compl_empty : ∀ {α : Type u}, ∅ᶜ = Set.univ This theorem states that the complement of the empty set, for any given type `α` is equivalent to the universal set. In set theory, the complement of a set `A` is made up of all the elements not in `A`. Here, as the set is empty, its complement includes every possible element of type `α`, hence it is equivalent to the universal set `Set.univ`. More concisely: The empty set and the universal set of type `α` are equivalent.
`Set.union_singleton` theorem Set.union_singleton : ∀ {α : Type u} {a : α} {s : Set α}, s ∪ {a} = insert a s This theorem states that for any set `s` of a given type `α` and any element `a` of type `α`, the union of `s` and the singleton set containing `a` is equivalent to inserting `a` into `s`. Here, the `insert a s` operation signifies the addition of the element `a` to the set `s`, and the `∪` symbol denotes the union operation between two sets. More concisely: For any set `s` of type `α` and any element `a` of type `α`, the union of `s` and the singleton set `{a}` is equal to the set `insert a s`.
`Mathlib.Data.Set.Basic._auxLemma.56` theorem Mathlib.Data.Set.Basic._auxLemma.56 : ∀ {α : Type u} {a : α} {s : Set α}, (s ∩ {a} = ∅) = (a ∉ s) The theorem `Mathlib.Data.Set.Basic._auxLemma.56` states that for any type `α`, an element `a` of type `α`, and a set `s` of type `α`, the intersection of set `s` and the singleton set containing `a` being an empty set is equivalent to `a` not being an element of set `s`. In other words, an element is not in a certain set if and only if the intersection of that set with a set containing only that element is empty. More concisely: For any type α and set s of α, the element a is not in s if and only if s ∩ {a} = ∅.
`Set.antitone_bforall` theorem Set.antitone_bforall : ∀ {α : Type u_1} {P : α → Prop}, Antitone fun s => ∀ x ∈ s, P x This theorem states that for any type `α` and any property `P` of type `α`, the function that maps a set to the proposition "every element in the set satisfies `P`" is antitone. In other words, if `s` and `t` are sets of type `α` where `s` is a subset of `t`, then "every element in `t` satisfies `P`" implies "every element in `s` satisfies `P`". This is consistent with the definition of an antitone function: if `a ≤ b` then `f(b) ≤ f(a)`, here `a` and `b` are sets and `≤` is the subset relation. More concisely: For any property `P` of type `α`, the function mapping a set to the proposition "every element in the set satisfies `P`" is antitone with respect to set inclusion.
`Set.pair_comm` theorem Set.pair_comm : ∀ {α : Type u} (a b : α), {a, b} = {b, a} This theorem, named `Set.pair_comm`, asserts the commutativity of a pair of elements from a given set in Lean 4. Specifically, for any type `α` and any two elements `a` and `b` of type `α`, the set `{a, b}` is equal to the set `{b, a}`. This means that the order of elements does not matter in the set formation - a mathematical concept that corresponds with the principle of commutativity in set theory. More concisely: For any set `α` and any two elements `a` and `b` in `α`, the sets `{a, b}` and `{b, a}` are equal.
`Set.Subset.trans` theorem Set.Subset.trans : ∀ {α : Type u} {a b c : Set α}, a ⊆ b → b ⊆ c → a ⊆ c This theorem, named as "Set.Subset.trans", states that for any type `α` and for any three sets `a`, `b`, and `c` of type `α`, if `a` is a subset of `b` and `b` is a subset of `c`, then `a` is also a subset of `c`. This is the transitive property of the subset relation among sets. In mathematical notation, for all sets $a$, $b$, and $c$, this can be expressed as: if $a \subseteq b$ and $b \subseteq c$, then $a \subseteq c$. More concisely: If sets `a`, `b`, and `c` are such that `a` is a subset of `b` and `b` is a subset of `c`, then `a` is a subset of `c` (transitive property of subset relation).
`Set.eq_empty_or_nonempty` theorem Set.eq_empty_or_nonempty : ∀ {α : Type u} (s : Set α), s = ∅ ∨ s.Nonempty This theorem states that for any set `s` of a certain type `α`, the set `s` is either equal to the empty set or it is not empty (i.e., it has at least one element). In other words, any set is either empty or nonempty, there is no third option. This is a formal logical expression of the law of the excluded middle for sets. Here, `Set.Nonempty s` is a way of saying that there exists an element `x` such that `x` belongs to `s`. More concisely: Every set is nonempty or equal to the empty set.
`Set.compl_union_self` theorem Set.compl_union_self : ∀ {α : Type u} (s : Set α), sᶜ ∪ s = Set.univ The theorem `Set.compl_union_self` states that for any set `s` of any type `α`, the union of the set `s` and its complement `sᶜ` (i.e., the set of all elements not in `s`) is `Set.univ`, the universal set of type `α`. In other words, every element of type `α` is either in `s` or not in `s`. This is a formalization of the principle of excluded middle in the context of sets. More concisely: For any set `s` of type `α`, `s ∪ sᶜ = Set.univ` (the universal set of type `α`).
`Set.union_diff_cancel` theorem Set.union_diff_cancel : ∀ {α : Type u} {s t : Set α}, s ⊆ t → s ∪ t \ s = t The theorem `Set.union_diff_cancel` states that for any type `α` and any two sets `s` and `t` of type `α`, if `s` is a subset of `t`, then the union of `s` and the difference of `t` and `s` equals `t`. In other words, if all elements of `s` are also in `t`, then adding `s` to `t` (which already includes `s`) and then removing `s` from the result leaves us with the original set `t`. This is a fundamental property of set operations in mathematics. More concisely: For any set `α` and sets `s` and `t` such that `s` is a subset of `t`, we have `s ⊆ t` implies `(s ∪ (t \ s)) = t`.
`Set.disjoint_of_subset_right` theorem Set.disjoint_of_subset_right : ∀ {α : Type u} {s t u : Set α}, t ⊆ u → Disjoint s u → Disjoint s t This theorem states that for any type `α` and any sets `s`, `t`, and `u` of type `α`, if set `t` is a subset of set `u` and `s` and `u` are disjoint, then `s` and `t` are also disjoint. In other words, if all elements of `t` are also in `u`, and there's no element that is both in `s` and `u`, then there can't be an element that is in both `s` and `t`. This is a statement about the relationship between set inclusion and disjointness in a lattice structure. More concisely: If sets `s` and `t` are disjoint and `t` is a subset of `u`, then `s` and `u` being disjoint implies `s` and `t` are disjoint.
`Set.exists_of_ssubset` theorem Set.exists_of_ssubset : ∀ {α : Type u} {s t : Set α}, s ⊂ t → ∃ x ∈ t, x ∉ s This theorem states that for any type `α`, and any two sets `s` and `t` of type `α`, if `s` is a strict subset of `t` (denoted `s ⊂ t`), then there exists an element `x` that belongs to `t` but does not belong to `s`. In mathematical terms, it asserts that if a set `s` is strictly contained within another set `t`, then there must be at least one element in `t` which is not in `s`. More concisely: Given any types `α` and sets `s` and `t` of type `α` with `s ⊂ t`, there exists an element `x ∈ t` such that `x ∉ s`.
`Set.insert_eq_self` theorem Set.insert_eq_self : ∀ {α : Type u} {a : α} {s : Set α}, insert a s = s ↔ a ∈ s This theorem states that for any type `α`, an element `a` of type `α`, and a set `s` of type `α`, inserting the element `a` into the set `s` results in the same set `s` if and only if the element `a` is already in the set `s`. In other words, it asserts that a set remains unchanged by inserting an element that it already contains. More concisely: For any set `s` and element `a` of type `α`, `a ∈ s` if and only if `s.insert a = s`.
`Set.not_mem_subset` theorem Set.not_mem_subset : ∀ {α : Type u} {a : α} {s t : Set α}, s ⊆ t → a ∉ t → a ∉ s This theorem states that for any type `α`, any element `a` of that type, and any sets `s` and `t` of the same type, if `s` is a subset of `t` and `a` is not an element of `t`, then `a` is also not an element of `s`. In mathematical terms, if $s \subseteq t$ and $a \notin t$, then it must be the case that $a \notin s$. More concisely: If a set `s` is a subset of set `t` and an element `a` is not in `t`, then `a` is not in `s`. In mathematical notation, $a \notin s$ given $s \subseteq t$ and $a \notin t$.
`Set.univ_nonempty` theorem Set.univ_nonempty : ∀ {α : Type u} [inst : Nonempty α], Set.univ.Nonempty This theorem, `Set.univ_nonempty`, states that for all types `α`, given an instance asserting that `α` is not empty (i.e. there exists at least one element of type `α`), the universal set on `α`, denoted as `Set.univ`, is also nonempty. In other words, if there is at least one element of some type `α`, then the set of all elements of type `α` also contains at least one element. More concisely: If `α` is a non-empty type, then `Set.univ α` is also a non-empty set.
`Set.mem_union_right` theorem Set.mem_union_right : ∀ {α : Type u} {x : α} {b : Set α} (a : Set α), x ∈ b → x ∈ a ∪ b The theorem `Set.mem_union_right` states that for any type `α`, any element `x` of type `α`, and any sets `a` and `b` of elements of type `α`, if `x` is a member of the set `b`, then `x` is also a member of the union of sets `a` and `b`. Here, the union of two sets (denoted as `a ∪ b`) is the set containing all elements that are in `a`, in `b`, or in both. More concisely: If `x` is an element of set `b`, then `x` is an element of the set `a ∪ b`.
`Set.disjoint_singleton_right` theorem Set.disjoint_singleton_right : ∀ {α : Type u} {a : α} {s : Set α}, Disjoint s {a} ↔ a ∉ s This theorem states that for any type `α`, any element `a` of that type, and any set `s` of elements of that type, the set `s` and the singleton set `{a}` are disjoint if and only if `a` is not an element of `s`. Here, two sets are considered disjoint if their intersection, or infimum, is the empty set (the bottom element in the context of sets). Hence, the theorem provides a characterization of disjointness in terms of non-membership of an element in a set. More concisely: For any type `α`, sets `s` of elements of `α`, and `a` in `α`, the sets `s` and `{a}` are disjoint if and only if `a` is not in `s`.
`LT.lt.ssubset` theorem LT.lt.ssubset : ∀ {α : Type u} {s t : Set α}, s < t → s ⊂ t This theorem, named `LT.lt.ssubset`, states that for any type `α` and any two sets `s` and `t` of type `α`, if `s` is less than `t` (denoted `s < t`), then `s` is a strict subset of `t` (denoted `s ⊂ t`). In other words, it provides an alias for the forward direction of the theorem `Set.lt_iff_ssubset`, asserting that a set being "less than" another set implies it being a strict subset of the latter. More concisely: If `s` is a subset of `t` and every element of `t` is in `s`, but there exists an element in `s` not in `t`, then `s` is strictly smaller than `t`.
`Set.disjoint_iff_inter_eq_empty` theorem Set.disjoint_iff_inter_eq_empty : ∀ {α : Type u} {s t : Set α}, Disjoint s t ↔ s ∩ t = ∅ This theorem states that for any type `α` and any two sets `s` and `t` of type `α`, the two sets are disjoint if and only if their intersection is the empty set. Here, two sets are considered disjoint if their infimum (greatest lower bound) is the bottom element. In terms of set theory, the "bottom element" can be understood as the empty set, and the "infimum" of two sets corresponds to their intersection. More concisely: For sets `s` and `t` of type `α`, `s` and `t` are disjoint if and only if `s ∩ t = ⊥`, where `⊥` denotes the bottom element.
`Set.not_monotoneOn_not_antitoneOn_iff_exists_lt_lt` theorem Set.not_monotoneOn_not_antitoneOn_iff_exists_lt_lt : ∀ {α : Type u} {β : Type v} {s : Set α} [inst : LinearOrder α] [inst_1 : LinearOrder β] {f : α → β}, ¬MonotoneOn f s ∧ ¬AntitoneOn f s ↔ ∃ a ∈ s, ∃ b ∈ s, ∃ c ∈ s, a < b ∧ b < c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c) The theorem states that for a function `f` defined on a set `s` with elements from a linearly ordered type `α` mapping to another linearly ordered type `β`, the function is neither monotone nor antitone on `s` if and only if there exist elements `a`, `b`, and `c` in `s` such that `a < b < c` and `f` forms a 'dent' at `b`, i.e., either `f(a) < f(b) < f(c)` (an upright dent) or `f(c) < f(b) < f(a)` (a downright dent). In other words, the function doesn't preserve the order in either direction for some triplet of elements in the set `s`. More concisely: A function `f` from a linearly ordered set `α` to another linearly ordered set `β` is neither monotone nor antitone if and only if there exist elements `a < b < c` in `α` such that `f(a)` and `f(c)` are on opposite sides of `f(b)`.
`Set.inter_subset_left` theorem Set.inter_subset_left : ∀ {α : Type u} (s t : Set α), s ∩ t ⊆ s The theorem `Set.inter_subset_left` states that for all types `α` and for any two sets `s` and `t` of type `α`, the intersection of `s` and `t` is a subset of `s`. In other words, every element that is both in set `s` and set `t` (i.e., in the intersection of `s` and `t`) is guaranteed to be in set `s`. More concisely: For all types α and sets s and t of type α, s ∩ t is a subset of s.
`Set.univ_inter` theorem Set.univ_inter : ∀ {α : Type u} (a : Set α), Set.univ ∩ a = a This theorem states that for all types `α` and for any set `a` of type `α`, the intersection of the universal set `Set.univ` with the set `a` is equal to `a` itself. In other words, when you intersect any set with the universal set (which contains all elements of the type), you simply get the original set back. In mathematical notation, this can be written as: ∀α, ∀a ∈ Set α, Set.univ ∩ a = a. More concisely: For all types `α` and sets `a` of type `α`, the intersection of the universal set `Set.univ` with `a` equals `a` (i.e., `Set.univ ∩ a = a`).
`Set.empty_inter` theorem Set.empty_inter : ∀ {α : Type u} (a : Set α), ∅ ∩ a = ∅ This theorem states that for any set `a` of any type `α`, the intersection of the empty set (`∅`) and `a` is always the empty set. This is in line with the general mathematical concept that the intersection of any set with the empty set is the empty set itself, as there are no elements common to the empty set and any other set. More concisely: The intersection of an empty set with any set `a` is the empty set. (∅ ∩ a = ∅)
`Set.nonempty_compl` theorem Set.nonempty_compl : ∀ {α : Type u} {s : Set α}, sᶜ.Nonempty ↔ s ≠ Set.univ This theorem states that for any type `α` and any set `s` of type `α`, the complement of the set `s` (denoted as `sᶜ`) is nonempty if and only if `s` is not the universal set. In other words, there exists at least one element not in `s` if and only if `s` does not contain all possible elements of the type `α` (i.e., `s` is not the universal set). This captures the intuitive notion that if a set doesn't contain everything, then there must be something it doesn't contain, and vice versa. More concisely: The complement of a set `s` of type `α` is nonempty if and only if `α` is not the universal set of `s`.
`HasSubset.Subset.disjoint_compl_left` theorem HasSubset.Subset.disjoint_compl_left : ∀ {α : Type u} {s t : Set α}, t ⊆ s → Disjoint sᶜ t This theorem, named `HasSubset.Subset.disjoint_compl_left`, states that for any type `α` and for any two sets `s` and `t` of type `α`, if `t` is a subset of `s`, then `s` complement (`sᶜ`) and `t` are disjoint. In the context of this theorem, two sets are said to be disjoint if their intersection is the empty set. More concisely: If `s` contains `t`, then the complement of `s` is disjoint from `t`.
`Set.diff_union_inter` theorem Set.diff_union_inter : ∀ {α : Type u} (s t : Set α), s \ t ∪ s ∩ t = s This theorem states that for any type `α` and any two sets `s` and `t` of type `α`, the union of the difference of `s` and `t` and the intersection of `s` and `t` is equal to `s`. In other words, if we remove elements in `t` from `s` and add back elements that `s` and `t` have in common, we end up with the original set `s` itself. In mathematical terms, for any sets `s` and `t`, we have $s \setminus t \cup (s \cap t) = s$. More concisely: The theorem asserts that for any sets `s` and `t`, their intersection added to the difference of `s` and `t` equals `s`, that is, $s \setminus t \cup s \cap t = s$.
`Mathlib.Data.Set.Basic._auxLemma.27` theorem Mathlib.Data.Set.Basic._auxLemma.27 : ∀ {α : Type u} (s t : Set α), (s ∩ t ⊆ t) = True The theorem `Mathlib.Data.Set.Basic._auxLemma.27` states that for any type `α` and any two sets `s` and `t` of type `α`, the intersection of the sets `s` and `t` (denoted by `s ∩ t`) is always a subset of the set `t`. This is a fundamental property of set theory, expressed in the language of Lean theorem prover. In symbols, this can be written as ∀s,t ∈ ℘(α), (s ∩ t) ⊆ t. More concisely: For any types `α` and sets `s` and `t` of type `α`, the intersection `s ∩ t` is a subset of `t`. In symbols, `(s ∩ t) ⊆ t`.
`Mathlib.Data.Set.Basic._auxLemma.29` theorem Mathlib.Data.Set.Basic._auxLemma.29 : ∀ {α : Type u} {s t : Set α}, (s ∩ t = s) = (s ⊆ t) This theorem, `Mathlib.Data.Set.Basic._auxLemma.29`, states that for any type `α` and for any two sets `s` and `t` of type `α`, the statement that the intersection of `s` and `t` equals `s` is equivalent to the statement that `s` is a subset of `t`. In other words, a set `s` is a subset of another set `t` if and only if all elements of `s` are also in `t`, which is exactly when the intersection of `s` and `t` gives `s` back. More concisely: The theorem asserts that for any sets `s` and `t` of type `α`, `s ⊆ t` if and only if `s = s ∩ t`.
`Set.mem_inter` theorem Set.mem_inter : ∀ {α : Type u} {x : α} {a b : Set α}, x ∈ a → x ∈ b → x ∈ a ∩ b The theorem `Set.mem_inter` states that for any type `α`, any element `x` of type `α`, and any two sets `a` and `b` of type `Set α`, if `x` is a member of both `a` and `b`, then `x` is also a member of the intersection of `a` and `b`. This theorem essentially formalizes one of the fundamental properties of set theory: the definition of set intersection. More concisely: If `x` is an element of both sets `a` and `b`, then `x` is an element of their intersection `a INTER b`.
`Set.diff_subset` theorem Set.diff_subset : ∀ {α : Type u} (s t : Set α), s \ t ⊆ s The theorem `Set.diff_subset` states that for any type `α`, and any two sets `s` and `t` of type `α`, the set difference of `s` and `t` (denoted as `s \ t`) is a subset of `s`. In mathematical terms, for all elements `x` of type `α`, if `x` is in the set difference `s \ t`, then `x` is also in `s`. More concisely: For any type `α` and sets `s` and `t` of type `α`, `s \ t` is a subset of `s`.
`Set.union_subset_union` theorem Set.union_subset_union : ∀ {α : Type u} {s₁ s₂ t₁ t₂ : Set α}, s₁ ⊆ s₂ → t₁ ⊆ t₂ → s₁ ∪ t₁ ⊆ s₂ ∪ t₂ This theorem states that for all types `α` and any sets `s₁`, `s₂`, `t₁`, and `t₂` of type `α`, if `s₁` is a subset of `s₂` and `t₁` is a subset of `t₂`, then the union of `s₁` and `t₁` is also a subset of the union of `s₂` and `t₂`. In mathematical terms, if $s_1 \subseteq s_2$ and $t_1 \subseteq t_2$, then $s_1 \cup t_1 \subseteq s_2 \cup t_2$. More concisely: Given sets `s₁`, `s₂`, `t₁`, and `t₂` of type `α`, if `s₁ ⊆ s₂` and `t₁ ⊆ t₂`, then `s₁ ∪ t₁ ⊆ s₂ ∪ t₂`.
`Set.insert_diff_of_mem` theorem Set.insert_diff_of_mem : ∀ {α : Type u} {a : α} {t : Set α} (s : Set α), a ∈ t → insert a s \ t = s \ t := by sorry The theorem `Set.insert_diff_of_mem` states that for any type `α`, any element `a` of type `α`, and any two sets `s` and `t` of type `α`, if `a` is an element of `t`, then the difference of the set resulting from inserting `a` into `s` and `t` is equal to the difference of `s` and `t`. In other words, if `a` is already in `t`, inserting `a` into `s` does not affect the relative complement of `s` in `t`. More concisely: If `a` is an element of set `t`, then `Set.insert a s = s \ t = s \ {a}`.
`Set.bot_eq_empty` theorem Set.bot_eq_empty : ∀ {α : Type u}, ⊥ = ∅ This theorem states that for any type `α`, the bottom element (`⊥`) is equal to the empty set (`∅`). In other words, in the context of set theory, `⊥` is used to denote the smallest element in a set, which is the empty set. This holds true for any type `α`. More concisely: For any type `α`, the bottom element `⊥` is equivalent to the empty set `∅`.
`SetCoe.forall'` theorem SetCoe.forall' : ∀ {α : Type u} {s : Set α} {p : (x : α) → x ∈ s → Prop}, (∀ (x : α) (h : x ∈ s), p x h) ↔ ∀ (x : ↑s), p ↑x ⋯ := by sorry This theorem states that for any type `α` and any set `s` of type `α`, a proposition `p` that depends upon an element `x` of `α` and the fact that `x` belongs to `s` holds for all elements `x` of `α` that belong to `s` if and only if it holds for all elements `x` of the coerced set `s`. In other words, it is stating that it is equivalent to consider the proposition `p` for all elements of the set `s` and for all elements of the set when considered as a subset of the type `α`. More concisely: For any set `s` of type `α` and proposition `p` depending on an element `x` in `α` and its membership in `s`, `p` holds for all `x` in `s` if and only if it holds for all `x` in the coerced set `s` viewed as a subset of `α`.
`Set.diff_subset_diff_left` theorem Set.diff_subset_diff_left : ∀ {α : Type u} {s₁ s₂ t : Set α}, s₁ ⊆ s₂ → s₁ \ t ⊆ s₂ \ t This theorem, `Set.diff_subset_diff_left`, states that for any type `α`, and for any sets `s₁`, `s₂`, and `t` of type `α`, if `s₁` is a subset of `s₂`, then the difference of `s₁` and `t` is also a subset of the difference of `s₂` and `t`. In other words, if every element of `s₁` is also an element of `s₂`, then every element that is in `s₁` but not in `t` is also in `s₂` but not in `t`. This is a property of set difference in the context of subset relationships. More concisely: If `s₁ ⊆ s₂`, then `(s₁ \ t) ⊆ (s₂ \ t)`. (In set theory notation, the symbol `\` represents set difference.)
`Set.insert_nonempty` theorem Set.insert_nonempty : ∀ {α : Type u} (a : α) (s : Set α), (insert a s).Nonempty The theorem `Set.insert_nonempty` states that for any given type `α` and any element `a` of this type, if we insert `a` into a set `s` of type `α`, the resulting set is nonempty. In other words, inserting any element into a set guarantees non-emptiness of the resulting set, regardless of the original state (empty or nonempty) of the set. This theorem applies to all types, making it a general property of sets in the context of Lean 4. More concisely: For any type `α` and element `a` of `α`, the set `a :: s` is nonempty, where `s` is a set of type `α`.
`Set.ext_iff` theorem Set.ext_iff : ∀ {α : Type u} {s t : Set α}, s = t ↔ ∀ (x : α), x ∈ s ↔ x ∈ t The theorem `Set.ext_iff` states that for any type `α`, and for any two sets `s` and `t` of type `α`, the sets `s` and `t` are equal if and only if for every element `x` of type `α`, `x` is a member of `s` if and only if `x` is a member of `t`. In other words, two sets are considered equal in Lean 4 if they have exactly the same elements. More concisely: Two sets of type `α` are equal if and only if they contain the same elements.
`Set.union_diff_right` theorem Set.union_diff_right : ∀ {α : Type u} {s t : Set α}, (s ∪ t) \ t = s \ t This theorem is about set operations in the context of some type `α`. Specifically, it states that for any two sets `s` and `t` of type `α`, the set difference of the union of `s` and `t` with `t` is equal to the set difference of `s` and `t`. In mathematical notation, this is saying that `(s ∪ t) \ t = s \ t` for all sets `s` and `t`. This is a property of the set union and set difference operations. More concisely: For all sets `s` and `t` of type `α`, the set difference of `s` and `t` is equal to the set difference of `s` and the subset `t` of its union with `t`. In other words, `(s ∪ t) \ t = s \ t`.
`Eq.subset` theorem Eq.subset : ∀ {α : Type u_1} {s t : Set α}, s = t → s ⊆ t This theorem states that for any type `α` and for any two sets `s` and `t` of this type, if `s` equals `t`, then `s` is a subset of `t`. Here, 'subset' means that every element of `s` is also an element of `t`. This is a duplicate of the theorem `Eq.subset'`, which is currently experiencing elaboration problems. More concisely: If `α` is a type and `s` and `t` are sets of `α` such that `s = t`, then `s` is a subset of `t`.
`Set.compl_subset_compl` theorem Set.compl_subset_compl : ∀ {α : Type u} {s t : Set α}, sᶜ ⊆ tᶜ ↔ t ⊆ s The theorem `Set.compl_subset_compl` states that for any given type `α` and any given sets `s` and `t` of type `α`, the complement of set `s` is a subset of the complement of set `t` if and only if set `t` is a subset of set `s`. Here, the complement of a set `s` (denoted as `sᶜ`) refers to the elements of type `α` that are not in `s`, and '⊆' denotes the subset relation. The theorem provides a fundamental relationship between set inclusion and their complements. More concisely: For sets `s` and `t` of type `α`, `sᶜ ⊆ tᶜ` if and only if `t ⊆ s`.
`Set.diff_singleton_eq_self` theorem Set.diff_singleton_eq_self : ∀ {α : Type u} {a : α} {s : Set α}, a ∉ s → s \ {a} = s The theorem `Set.diff_singleton_eq_self` states that for any type `α`, any element `a` of type `α`, and any set `s` of elements of type `α`, if `a` does not belong to `s` (`a ∉ s`), then the difference of `s` and the singleton set containing `a` (`s \ {a}`) is equal to `s` itself. In other words, removing an element that is not in the set does not change the set. More concisely: For any set `s` and element `a` in a type `α`, if `a ∉ s`, then `s \ {a} = s`.
`Set.eq_singleton_iff_unique_mem` theorem Set.eq_singleton_iff_unique_mem : ∀ {α : Type u} {a : α} {s : Set α}, s = {a} ↔ a ∈ s ∧ ∀ x ∈ s, x = a := by sorry This theorem, `Set.eq_singleton_iff_unique_mem`, states that for any given type `α`, any element `a` of type `α`, and any set `s` of type `α`, the set `s` is equal to a singleton set containing only the element `a` if and only if `a` is an element of `s` and for all elements `x` in `s`, `x` is equal to `a`. In other words, a set is a singleton set containing a certain element if and only if that element is in the set and all other elements in the set are equal to that element. More concisely: A set equals the singleton set consisting of an element if and only if that element is in the set and belongs to no other element.
`Set.coe_setOf` theorem Set.coe_setOf : ∀ {α : Type u} (p : α → Prop), ↑{x \| p x} = { x // p x } This theorem states that for any type `α` and any property `p` that elements of this type may satisfy, the set of all elements `x` of type `α` that satisfy `p` (symbolized by `{x \| p x}`) is equivalent to the set of all elements `x` along with a proof that `x` satisfies `p` (symbolized by `{ x // p x }`). This is essentially a type-level statement that these two ways of defining a subset of a type are interchangeable. More concisely: The type of subsets of any type `α` defined as `{x \| p x}` is equivalent to the type of pairs `{x // p x}` where `x` is an element of `α` and `p x` is a proof that `p` holds for `x`.
`Set.subset_compl_comm` theorem Set.subset_compl_comm : ∀ {α : Type u} {s t : Set α}, s ⊆ tᶜ ↔ t ⊆ sᶜ This theorem states that for any type `α` and any two sets `s` and `t` of the type `α`, `s` is a subset of the complement of `t` if and only if `t` is a subset of the complement of `s`. Here, the complement of a set `s` (denoted `sᶜ`) contains all elements of the type `α` that are not in `s`, and `s` is a subset of `t` (denoted `s ⊆ t`) if every element of `s` is also an element of `t`. More concisely: For any type `α` and sets `s` and `t` of type `α`, `s` is a subset of `sᶜ` if and only if `t` is a subset of `tᶜ`, where `sᶜ` denotes the complement of `s` and `tᶜ` denotes the complement of `t`.
`HasSubset.Subset.le` theorem HasSubset.Subset.le : ∀ {α : Type u} {s t : Set α}, s ⊆ t → s ≤ t This theorem, also known as an Alias of the reverse direction of `Set.le_iff_subset`, states that for any type `α` and any sets `s` and `t` of type `α`, if `s` is a subset of `t` (denoted by `s ⊆ t`), then `s` is less than or equal to `t` (denoted by `s ≤ t`). In other words, the subset relationship implies the less than or equal to relationship between two sets. More concisely: If `s` is a subset of `t`, then `s` is contained in `t`, which is denoted as `s ⊆ t`, implies `s` is less than or equal to `t`, denoted as `s ≤ t`.
`Mathlib.Data.Set.Basic._auxLemma.46` theorem Mathlib.Data.Set.Basic._auxLemma.46 : ∀ {α : Sort u_1} {p q : α → Prop}, (∃ x, p x ∨ q x) = ((∃ x, p x) ∨ ∃ x, q x) This theorem states that for any type `α` and two predicates `p` and `q` on `α`, the existence of an element that satisfies either `p` or `q` is equivalent to either the existence of an element that satisfies `p` or the existence of an element that satisfies `q`. This expresses the distributive property of existential quantification over disjunction. More concisely: For any type `α` and predicates `p` and `q` on `α`, the existence of an element satisfying `p` or `q` is equivalent to the existence of an element satisfying `p ∨ q`.
`Set.ssubset_iff_of_subset` theorem Set.ssubset_iff_of_subset : ∀ {α : Type u} {s t : Set α}, s ⊆ t → (s ⊂ t ↔ ∃ x ∈ t, x ∉ s) This theorem states that for any two sets `s` and `t` of some type `α`, if `s` is a subset of `t` (expressed as `s ⊆ t`), then the condition for `s` to be a proper subset of `t` (expressed as `s ⊂ t`) is equivalent to the existence of an element `x` that belongs to `t` but does not belong to `s` (expressed as `∃ x ∈ t, x ∉ s`). In other words, a set `s` is a proper subset of another set `t`, given that `s` is already a subset of `t`, if and only if there is at least one element in `t` that is not included in `s`. More concisely: A set is a proper subset of another set if and only if it is a subset and there exists an element in the larger set not in the smaller set.
`Set.diff_empty` theorem Set.diff_empty : ∀ {α : Type u} {s : Set α}, s \ ∅ = s This theorem states that for any set `s` of any type `α`, the difference of `s` with the empty set is `s` itself. In other words, if you subtract nothing (empty set) from a set, you get the original set back. Symbolically, this can be represented as `s \ ∅ = s` for any set `s`. More concisely: For any set `s` of type `α`, the set difference `s \ ∅` equals `s`.
`Set.not_disjoint_iff` theorem Set.not_disjoint_iff : ∀ {α : Type u} {s t : Set α}, ¬Disjoint s t ↔ ∃ x ∈ s, x ∈ t The theorem `Set.not_disjoint_iff` states that for any type `α` and any two sets `s` and `t` of type `α`, the sets `s` and `t` are not disjoint if and only if there exists an element `x` which belongs to both `s` and `t`. In other words, the negation of the disjointness of two sets is equivalent to the existence of a common element in the two sets. This is a generalization of the concept of disjoint sets in set theory, where two sets are said to be disjoint if they have no elements in common. More concisely: For any type `α` and sets `s` and `t` of type `α`, `s` and `t` are not disjoint if and only if there exists an element `x` in `α` that belongs to both `s` and `t`.
`Set.Subset.antisymm` theorem Set.Subset.antisymm : ∀ {α : Type u} {a b : Set α}, a ⊆ b → b ⊆ a → a = b The theorem `Set.Subset.antisymm` states that for all types `α` and for all sets `a` and `b` of type `α`, if `a` is a subset of `b` and `b` is a subset of `a`, then `a` and `b` are equal. This is a formalization of the concept of antisymmetry in the context of set theory. In mathematical terms, given any two sets `a` and `b`, if every element of `a` also belongs to `b` (i.e., `a` is a subset of `b`) and every element of `b` also belongs to `a` (i.e., `b` is a subset of `a`), then `a` and `b` are the same set. More concisely: If sets `a` and `b` have the property that every element in `a` is in `b` and every element in `b` is in `a`, then `a` and `b` are equal.
`Set.inter_subset_right` theorem Set.inter_subset_right : ∀ {α : Type u} (s t : Set α), s ∩ t ⊆ t This theorem states that for any type `α` and for any two sets `s` and `t` of type `α`, the intersection of `s` and `t` is a subset of `t`. More formally, for any element of `α`, if it is in both `s` and `t` (i.e., it is in the intersection of `s` and `t`), then it is in `t`. This is a fundamental property of set intersection in mathematics. More concisely: For any sets `s` and `t` of type `α`, the intersection of `s` and `t` is a subset of `t`. In other words, for all `x` in `α`, if `x` is in `s` and `x` is in `t`, then `x` is in `t`.
`Set.diff_subset_diff` theorem Set.diff_subset_diff : ∀ {α : Type u} {s₁ s₂ t₁ t₂ : Set α}, s₁ ⊆ s₂ → t₂ ⊆ t₁ → s₁ \ t₁ ⊆ s₂ \ t₂ This theorem states that for any type `α` and for any four sets `s₁`, `s₂`, `t₁`, `t₂` of this type, if `s₁` is a subset of `s₂` and `t₂` is a subset of `t₁`, then the difference of `s₁` and `t₁` is a subset of the difference of `s₂` and `t₂`. Here, the difference of two sets `A` and `B`, denoted `A \ B`, comprises all elements that are in `A` but not in `B`. More concisely: For any type `α` and sets `s₁`, `s₂`, `t₁`, `t₂` of type `α`, if `s₁ ⊆ s₂` and `t₂ ⊆ t₁`, then `(s₁ \ t₁) ⊆ (s₂ \ t₂)`.
`Antitone.inter` theorem Antitone.inter : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder β] {f g : β → Set α}, Antitone f → Antitone g → Antitone fun x => f x ∩ g x The theorem `Antitone.inter` states that for all types `α` and `β`, where `β` has a preorder structure, and any two functions `f` and `g` from `β` to the set of `α`, if both `f` and `g` are antitone (i.e., for all `a, b` in `β`, if `a ≤ b`, then `f(b) ≤ f(a)` and `g(b) ≤ g(a)`), then the function that maps `x` in `β` to the intersection of the sets `f(x)` and `g(x)` is also antitone. More concisely: If `f` and `g` are antitone functions from a preordered type `β` to type `α`, then the function that maps each `x` in `β` to the intersection of `f(x)` and `g(x)` is also an antitone function.
`Set.subset_univ` theorem Set.subset_univ : ∀ {α : Type u} (s : Set α), s ⊆ Set.univ This theorem, named `Set.subset_univ`, states that for any given type `α` and any set `s` of type `α`, `s` is a subset of the universal set `Set.univ` of type `α`. In other words, every element of the set `s` is also an element of the universal set `Set.univ`. Here, the symbol `⊆` denotes the subset relation. This is a fundamental property of universal sets, conforming to the idea that a universal set contains all elements of a given type. More concisely: For any type α and set s of type α, s is a subset of the universal set Set.univ of type α. (Written mathematically: s ⊆ Set.univ)
`Mathlib.Data.Set.Basic._auxLemma.25` theorem Mathlib.Data.Set.Basic._auxLemma.25 : ∀ {α : Type u} (x : α) (a b : Set α), (x ∈ a ∩ b) = (x ∈ a ∧ x ∈ b) := by sorry This theorem, named `Mathlib.Data.Set.Basic._auxLemma.25`, states that for any type `α`, and any element `x` of type `α`, and any two sets `a` and `b` of elements of type `α`, the membership of `x` in the intersection of `a` and `b` is equivalent to the conjunction of the membership of `x` in `a` and the membership of `x` in `b`. In other words, an element belongs to the intersection of two sets if and only if it belongs to both of these sets. More concisely: For any type `α` and sets `a` and `b` of elements of type `α`, an element `x` belongs to the intersection `a ∩ b` if and only if it belongs to both sets `a` and `b`: `x ∈ a ∧ x ∈ b ↔ x ∈ a ∧ b`.
`Set.univ_subset_iff` theorem Set.univ_subset_iff : ∀ {α : Type u} {s : Set α}, Set.univ ⊆ s ↔ s = Set.univ This theorem states that for any type `α` and any set `s` of type `α`, the universal set `Set.univ` is a subset of `s` if and only if `s` is equal to the universal set `Set.univ`. In other words, the only subset that includes every element of the universal set is the universal set itself. This is a standard result in set theory and highlights the maximal nature of the universal set, which by definition contains every element of the given type. More concisely: The universal set `Set.univ` is equal to any set `s` if and only if `s` contains the universal set `Set.univ`.
`Set.union_comm` theorem Set.union_comm : ∀ {α : Type u} (a b : Set α), a ∪ b = b ∪ a The theorem `Set.union_comm` states that for any type `α` and any two sets `a` and `b` of type `α`, the union of `a` and `b` is equal to the union of `b` and `a`. This is the commutative property of set union, which essentially means that the order in which sets are united does not affect the resulting set. More concisely: For any type `α` and sets `a` and `b` of type `α`, `a ∪ b = b ∪ a`.
`Set.not_monotoneOn_not_antitoneOn_iff_exists_le_le` theorem Set.not_monotoneOn_not_antitoneOn_iff_exists_le_le : ∀ {α : Type u} {β : Type v} {s : Set α} [inst : LinearOrder α] [inst_1 : LinearOrder β] {f : α → β}, ¬MonotoneOn f s ∧ ¬AntitoneOn f s ↔ ∃ a ∈ s, ∃ b ∈ s, ∃ c ∈ s, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c) The theorem states that for a function `f` acting on elements of a set `s` within a linearly ordered type, if the function is neither monotone nor antitone on `s` (that is, it neither preserves the order of elements nor inverts it), then there exist three elements `a`, `b`, and `c` in `s` such that `a ≤ b`, `b ≤ c` and either `f(a) < f(b)` and `f(c) < f(b)` (forming an upright "dent"), or `f(b) < f(a)` and `f(b) < f(c)` (forming a downward "dent"). More concisely: For a function on a linearly ordered type, if it is neither order-preserving nor order-reversing, then there exist elements with the property that their ordering is inverted by the function while maintaining the ordering among themselves.
`Set.compl_empty_iff` theorem Set.compl_empty_iff : ∀ {α : Type u} {s : Set α}, sᶜ = ∅ ↔ s = Set.univ This theorem states that for any type `α` and a set `s` of type `α`, the complement of `s` is empty if and only if `s` is the universal set. In other words, a set `s` is the universal set (meaning it contains all elements of the type `α`) precisely when its complement (the set of all elements not in `s`) is empty. This is a formalization of a basic principle from set theory. More concisely: A set is the universal set if and only if its complement is empty.
`Set.compl_inter_self` theorem Set.compl_inter_self : ∀ {α : Type u} (s : Set α), sᶜ ∩ s = ∅ This theorem states that for any set `s` of any type `α`, the intersection of the complement of `s` (denoted as `sᶜ`) with `s` itself, is equal to the empty set. In other words, there are no elements that are both in `s` and not in `s` at the same time, which conforms to the principle of contradiction in set theory. More concisely: For any set `s` of type `α`, the intersection of `s` and its complement `sᶜ` is the empty set. (Or, more succinctly: `s ∩ sᶜ = ∅`.)
`Set.mem_of_mem_inter_left` theorem Set.mem_of_mem_inter_left : ∀ {α : Type u} {x : α} {a b : Set α}, x ∈ a ∩ b → x ∈ a The theorem `Set.mem_of_mem_inter_left` states that for any type `α`, any element `x` of `α`, and any two sets `a` and `b` of type `α`, if `x` belongs to the intersection of `a` and `b`, then `x` also belongs to `a`. In other words, if an element is in both `a` and `b`, it is definitely in `a`. More concisely: If `a` and `b` are sets and `x` is an element belonging to `a ∩ b`, then `x` is also an element of `a`.
`Set.eq_of_subset_of_subset` theorem Set.eq_of_subset_of_subset : ∀ {α : Type u} {a b : Set α}, a ⊆ b → b ⊆ a → a = b The theorem `Set.eq_of_subset_of_subset` states that for any type `α` and any two sets `a` and `b` of that type, if `a` is a subset of `b` and `b` is a subset of `a`, then `a` and `b` are equal. Here, a set `a` being a subset of another set `b` (denoted as `a ⊆ b`) means that every element of `a` is also an element of `b`. Therefore, this theorem expresses the idea of set equality in terms of subset relationships. More concisely: If two sets `α` have the subset relation `a ⊆ b` and `b ⊆ a`, then `a = b`.
`Mathlib.Data.Set.Basic._auxLemma.104` theorem Mathlib.Data.Set.Basic._auxLemma.104 : ∀ {α : Sort u_1} {p q : α → Prop}, ((∀ (x : α), p x) ∧ ∀ (x : α), q x) = ∀ (x : α), p x ∧ q x This theorem states that for any type `α` and any two properties `p` and `q` that elements of `α` can have, the statement "all elements of `α` have property `p` and all elements of `α` have property `q`" is equivalent to the statement "all elements of `α` have both property `p` and property `q`". In other words, it formalizes the idea that if every element of a set satisfies two conditions separately, then every element of that set satisfies both conditions simultaneously. More concisely: For any type `α` and properties `p` and `q` on `α`, the statements "forall x : α, p x" and "forall x : α, q x" are equivalent to "forall x : α, p x ∧ q x".

LeanAide GPT-4 documentation

Module: Mathlib.Data.Set.Basic

Set.mem_insert_iff

theorem Set.mem_insert_iff : ∀ {α : Type u} {x a : α} {s : Set α}, x ∈ insert a s ↔ x = a ∨ x ∈ s

Set.not_subset

theorem Set.not_subset : ∀ {α : Type u} {s t : Set α}, ¬s ⊆ t ↔ ∃ a ∈ s, a ∉ t

Set.mem_union

theorem Set.mem_union : ∀ {α : Type u} (x : α) (a b : Set α), x ∈ a ∪ b ↔ x ∈ a ∨ x ∈ b

Subsingleton.mem_iff_nonempty

theorem Subsingleton.mem_iff_nonempty : ∀ {α : Type u_2} [inst : Subsingleton α] {s : Set α} {x : α}, x ∈ s ↔ s.Nonempty

Set.empty_diff

theorem Set.empty_diff : ∀ {α : Type u} (s : Set α), ∅ \ s = ∅

Set.inter_eq_self_of_subset_right

theorem Set.inter_eq_self_of_subset_right : ∀ {α : Type u} {s t : Set α}, t ⊆ s → s ∩ t = t

Set.not_mem_compl_iff

theorem Set.not_mem_compl_iff : ∀ {α : Type u} {s : Set α} {x : α}, x ∉ sᶜ ↔ x ∈ s

Set.diff_union_self

theorem Set.diff_union_self : ∀ {α : Type u} {s t : Set α}, s \ t ∪ t = s ∪ t

Set.nonempty_of_mem

theorem Set.nonempty_of_mem : ∀ {α : Type u} {s : Set α} {x : α}, x ∈ s → s.Nonempty

Set.ssubset_singleton_iff

theorem Set.ssubset_singleton_iff : ∀ {α : Type u} {s : Set α} {x : α}, s ⊂ {x} ↔ s = ∅

Set.empty_union

theorem Set.empty_union : ∀ {α : Type u} (a : Set α), ∅ ∪ a = a

Set.mem_empty_iff_false

theorem Set.mem_empty_iff_false : ∀ {α : Type u} (x : α), x ∈ ∅ ↔ False

Set.mem_of_subset_of_mem

theorem Set.mem_of_subset_of_mem : ∀ {α : Type u} {s₁ s₂ : Set α} {a : α}, s₁ ⊆ s₂ → a ∈ s₁ → a ∈ s₂

Set.compl_eq_univ_diff

theorem Set.compl_eq_univ_diff : ∀ {α : Type u} (s : Set α), sᶜ = Set.univ \ s

Set.disjoint_sdiff_inter

theorem Set.disjoint_sdiff_inter : ∀ {α : Type u} {s t : Set α}, Disjoint (s \ t) (s ∩ t)

Set.union_inter_distrib_right

theorem Set.union_inter_distrib_right : ∀ {α : Type u} (s t u : Set α), (s ∪ t) ∩ u = s ∩ u ∪ t ∩ u

Set.insert_comm

theorem Set.insert_comm : ∀ {α : Type u} (a b : α) (s : Set α), insert a (insert b s) = insert b (insert a s) := by sorry

Set.singleton_subset_iff

theorem Set.singleton_subset_iff : ∀ {α : Type u} {a : α} {s : Set α}, {a} ⊆ s ↔ a ∈ s

Subsingleton.eq_univ_of_nonempty

theorem Subsingleton.eq_univ_of_nonempty : ∀ {α : Type u_1} [inst : Subsingleton α] {s : Set α}, s.Nonempty → s = Set.univ

Set.inter_subset_inter

theorem Set.inter_subset_inter : ∀ {α : Type u} {s₁ s₂ t₁ t₂ : Set α}, s₁ ⊆ t₁ → s₂ ⊆ t₂ → s₁ ∩ s₂ ⊆ t₁ ∩ t₂

Set.inter_union_distrib_left

theorem Set.inter_union_distrib_left : ∀ {α : Type u} (s t u : Set α), s ∩ (t ∪ u) = s ∩ t ∪ s ∩ u

Set.inter_right_comm

theorem Set.inter_right_comm : ∀ {α : Type u} (s₁ s₂ s₃ : Set α), s₁ ∩ s₂ ∩ s₃ = s₁ ∩ s₃ ∩ s₂

Set.eq_univ_of_univ_subset

theorem Set.eq_univ_of_univ_subset : ∀ {α : Type u} {s : Set α}, Set.univ ⊆ s → s = Set.univ

Set.inter_compl_nonempty_iff

theorem Set.inter_compl_nonempty_iff : ∀ {α : Type u} {s t : Set α}, (s ∩ tᶜ).Nonempty ↔ ¬s ⊆ t

Set.insert_subset_iff

theorem Set.insert_subset_iff : ∀ {α : Type u} {a : α} {s t : Set α}, insert a s ⊆ t ↔ a ∈ t ∧ s ⊆ t

Set.mem_insert

theorem Set.mem_insert : ∀ {α : Type u} (x : α) (s : Set α), x ∈ insert x s

Set.diff_union_of_subset

theorem Set.diff_union_of_subset : ∀ {α : Type u} {s t : Set α}, t ⊆ s → s \ t ∪ t = s

Set.diff_subset_iff

theorem Set.diff_subset_iff : ∀ {α : Type u} {s t u : Set α}, s \ t ⊆ u ↔ s ⊆ t ∪ u

Set.subset_empty_iff

theorem Set.subset_empty_iff : ∀ {α : Type u} {s : Set α}, s ⊆ ∅ ↔ s = ∅

Set.union_assoc

theorem Set.union_assoc : ∀ {α : Type u} (a b c : Set α), a ∪ b ∪ c = a ∪ (b ∪ c)

Set.inter_subset_inter_right

theorem Set.inter_subset_inter_right : ∀ {α : Type u} {s t : Set α} (u : Set α), s ⊆ t → u ∩ s ⊆ u ∩ t

Set.union_eq_self_of_subset_left

theorem Set.union_eq_self_of_subset_left : ∀ {α : Type u} {s t : Set α}, s ⊆ t → s ∪ t = t

Membership.mem.out

theorem Membership.mem.out : ∀ {α : Type u} {p : α → Prop} {a : α}, a ∈ {x | p x} → p a

Set.Nonempty.mono

theorem Set.Nonempty.mono : ∀ {α : Type u} {s t : Set α}, s ⊆ t → s.Nonempty → t.Nonempty

Set.disjoint_sdiff_left

theorem Set.disjoint_sdiff_left : ∀ {α : Type u} {s t : Set α}, Disjoint (t \ s) s

Set.mem_setOf

theorem Set.mem_setOf : ∀ {α : Type u} {a : α} {p : α → Prop}, a ∈ {x | p x} ↔ p a

Set.inter_union_diff

theorem Set.inter_union_diff : ∀ {α : Type u} (s t : Set α), s ∩ t ∪ s \ t = s

Set.union_diff_left

theorem Set.union_diff_left : ∀ {α : Type u} {s t : Set α}, (s ∪ t) \ s = t \ s

Set.nonempty_iff_ne_empty'

theorem Set.nonempty_iff_ne_empty' : ∀ {α : Type u} {s : Set α}, Nonempty ↑s ↔ s ≠ ∅

`Set.mem_insert_iff`

`Set.not_subset`

`Set.mem_union`

`Subsingleton.mem_iff_nonempty`

`Set.empty_diff`

`Set.inter_eq_self_of_subset_right`

`Set.not_mem_compl_iff`

`Set.diff_union_self`

`Set.nonempty_of_mem`

`Set.ssubset_singleton_iff`

`Set.empty_union`

`Set.mem_empty_iff_false`

`Set.mem_of_subset_of_mem`

`Set.compl_eq_univ_diff`

`Set.disjoint_sdiff_inter`

`Set.union_inter_distrib_right`

`Set.insert_comm`

`Set.singleton_subset_iff`

`Subsingleton.eq_univ_of_nonempty`

`Set.inter_subset_inter`

`Set.inter_union_distrib_left`

`Set.inter_right_comm`

`Set.eq_univ_of_univ_subset`

`Set.inter_compl_nonempty_iff`

`Set.insert_subset_iff`

`Set.mem_insert`

`Set.diff_union_of_subset`

`Set.diff_subset_iff`

`Set.subset_empty_iff`

`Set.union_assoc`

`Set.inter_subset_inter_right`

`Set.union_eq_self_of_subset_left`

`Membership.mem.out`

`Set.Nonempty.mono`

`Set.disjoint_sdiff_left`

`Set.mem_setOf`

`Set.inter_union_diff`

`Set.union_diff_left`

`Set.nonempty_iff_ne_empty'`

`Set.nonempty_iff_univ_nonempty`

`Mathlib.Data.Set.Basic._auxLemma.81`

`Set.Nonempty.empty_ssubset`

`AntitoneOn.inter`

`Set.eq_empty_of_forall_not_mem`

`Set.union_eq_self_of_subset_right`

`Set.eq_empty_of_isEmpty`

`Disjoint.ne_of_mem`

`Set.mem_singleton`

`Set.disjoint_compl_right_iff_subset`

`Mathlib.Data.Set.Basic._auxLemma.49`

`Set.inter_union_compl`

`Set.empty_ne_univ`

`LE.le.subset`

`Set.disjoint_left`

`Set.insert_eq`

`Set.compl_union`

`Set.union_compl_self`

`Set.insert_eq_of_mem`

`Set.singleton_union`

`Mathlib.Data.Set.Basic._auxLemma.28`

`Mathlib.Data.Set.Basic._auxLemma.65`

`Set.inter_empty`

`Set.mem_compl`

`Set.union_subset`

`Set.nonempty_of_nonempty_subtype`

`Mathlib.Data.Set.Basic._auxLemma.83`

`Set.sep_eq_self_iff_mem_true`

`Set.Nonempty.not_disjoint`

`Disjoint.subset_compl_left`

`Mathlib.Data.Set.Basic._auxLemma.31`

`Set.singleton_ne_empty`

`Set.pair_eq_singleton`

`Set.inter_comm`

`Set.inter_self`