Sym2.other_spec
theorem Sym2.other_spec : ∀ {α : Type u_1} {a : α} {z : Sym2 α} (h : a ∈ z), s(a, Sym2.Mem.other h) = z
The theorem `Sym2.other_spec` states that for any type `α`, any element `a` of type `α`, and any unordered pair `z` of type `Sym2 α` (which is the type of unordered pairs of `α`), if `a` is a member of `z`, then the unordered pair created from `a` and the other member of `z` (found using the `Sym2.Mem.other` function) is equal to `z`. Essentially, it says that if we disassemble an unordered pair into its components and then reassemble it, we get the original unordered pair.
More concisely: For any type `α` and unordered pair `z` of type `Sym2 α` with member `a`, `{a} ⊓ z = z`. Here, `⊓` denotes the "symmetric difference with" operator in Set theory, which returns the elements common to both sets.
|
Sym2.eq_swap
theorem Sym2.eq_swap : ∀ {α : Type u_1} {a b : α}, s(a, b) = s(b, a)
This theorem, `Sym2.eq_swap`, states that for any type `α` and any two elements `a` and `b` of that type, the function `s` applied to `a` and `b` is equal to the function `s` applied to `b` and `a`. This essentially encapsulates the property of commutativity for the function `s` on any pair of elements of a given type.
More concisely: For any type `α` and any elements `a` and `b` of type `α`, the function application `s a b` is equal to `s b a`.
|
Sym2.mk_isDiag_iff
theorem Sym2.mk_isDiag_iff : ∀ {α : Type u_1} {x y : α}, s(x, y).IsDiag ↔ x = y
The theorem `Sym2.mk_isDiag_iff` states that for any type `α` and any two elements `x` and `y` of that type, a pair `(x, y)` is on the diagonal of the symmetric square `Sym2 α` if and only if `x` equals `y`. In other words, a `Sym2` pair is on the diagonal when its two elements are the same.
More concisely: The theorem `Sym2.mk_isDiag_iff` asserts that two elements `x` and `y` of type `α` lie on the diagonal of the symmetric square `Sym2 α` if and only if `x = y`.
|
Mathlib.Data.Sym.Sym2._auxLemma.19
theorem Mathlib.Data.Sym.Sym2._auxLemma.19 :
∀ {α : Type u_1} {r : α → α → Prop} {sym : Symmetric r} {z : α × α}, (Sym2.mk z ∈ Sym2.fromRel sym) = r z.1 z.2
This theorem, `Mathlib.Data.Sym.Sym2._auxLemma.19`, states that for any type `α`, a symmetric relation `r` on `α`, and a pair `z` of type `α × α`, the membership of the pair `z` in the set derived from the symmetric relation `r` by the function `Sym2.fromRel` is equivalent to the relation `r` holding between the first and the second element of the pair `z`. In other words, a pair `z` is in the set defined by the symmetric relation `r` if and only if the relation `r` is true when applied to the elements of `z`.
More concisely: For any type `α` and symmetric relation `r` on `α`, `(z : α × α) ∈ Set.image (Sym2.fromRel r) z if and only if r z.1 z.2`.
|
Sym2.ind
theorem Sym2.ind : ∀ {α : Type u_1} {f : Sym2 α → Prop}, (∀ (x y : α), f s(x, y)) → ∀ (i : Sym2 α), f i
The theorem `Sym2.ind` states that for any type `α` and any property `f` defined on unordered pairs of elements of `α` (expressed as `Sym2 α`), if the property `f` holds for any pair `(x, y)` of elements of `α`, then it holds for any unordered pair `i` in `Sym2 α`. This is a form of principle of mathematical induction tailored for the symmetric square of a type.
More concisely: If `f` is a property of unordered pairs of elements in type `α`, and `f x y` holds for all pairs `(x, y)` in `Sym2 α`, then `f i` holds for all `i` in `Sym2 α`.
|
Sym2.mem_and_mem_iff
theorem Sym2.mem_and_mem_iff : ∀ {α : Type u_1} {x y : α} {z : Sym2 α}, x ≠ y → (x ∈ z ∧ y ∈ z ↔ z = s(x, y)) := by
sorry
This theorem states that for any type `α`, given distinct elements `x` and `y` from `α` and an element `z` of the symmetric square of `α` (`Sym2 α`), `x` and `y` are both elements of `z` if and only if `z` is the unordered pair of `x` and `y`. In other words, an element of the symmetric square of a type contains a specific distinct pair of elements if and only if it is that specific pair. This theorem thus relates the membership of elements in a pair to the identity of the pair.
More concisely: For any type `α` and distinct elements `x, y` from `α`, an element `z` of `Sym2 α` contains both `x` and `y` if and only if `z` is the unordered pair `{x, y}`.
|
Sym2.map_id'
theorem Sym2.map_id' : ∀ {α : Type u_1}, (Sym2.map fun x => x) = id
This theorem, named `Sym2.map_id'`, states that for all types `α`, applying the `Sym2.map` function with the identity function as the argument is equivalent to the identity function itself. In mathematical terms, for any symmetric pair of elements in type `α`, applying the `Sym2.map` function with the identity function leaves the symmetric pair unchanged, just like the identity function. However, note that `Sym2.map id z` will not simplify due to `Sym2.map_congr`.
More concisely: For all types `α`, the application of `Sym2.map` with the identity function on a symmetric pair of elements is equal to the identity function itself.
|
Mathlib.Data.Sym.Sym2._auxLemma.13
theorem Mathlib.Data.Sym.Sym2._auxLemma.13 : ∀ {α : Type u_1} {a b c : α}, (a ∈ s(b, c)) = (a = b ∨ a = c)
This theorem, named `Mathlib.Data.Sym.Sym2._auxLemma.13`, states that for any type `α` and any three elements `a`, `b`, and `c` of type `α`, the statement "`a` is an element of the symmetric pair `(b, c)`" is equivalent to saying "`a` is equal to `b` or `a` is equal to `c`". Thus, an element is in the symmetric pair if and only if it is equal to one of the elements of the pair.
More concisely: For any type α and elements a, b, c of α, a is in the symmetric pair (b, c) if and only if a is equal to b or a is equal to c.
|
Sym2.mem_mk_right
theorem Sym2.mem_mk_right : ∀ {α : Type u_1} (x y : α), y ∈ s(x, y)
This theorem, `Sym2.mem_mk_right`, asserts that for any type `α` and any two elements `x` and `y` of that type, `y` is a member of the unordered pair `(x, y)`. In other words, the theorem guarantees that if we create an unordered pair from two elements, the second element will always be considered a member of that pair.
More concisely: For any type `α` and any `x, y : α`, `y` is a member of the unordered pair `{x, y}`.
|
Sym2.other_spec'
theorem Sym2.other_spec' :
∀ {α : Type u_1} [inst : DecidableEq α] {a : α} {z : Sym2 α} (h : a ∈ z), s(a, Sym2.Mem.other' h) = z
This theorem states that for any type `α` with a decidable equality and for any elements `a` of type `α` and `z` of type `Sym2 α` (i.e., an unordered pair of `α`), if `a` is a member of `z`, then the result of pairing `a` with the other element of the unordered pair `z` (obtained using the function `Sym2.Mem.other'`) is equal to `z`. In other words, it ensures that the function `Sym2.Mem.other'` correctly retrieves the other element of the unordered pair `z` when `a` is known to be a member of `z`.
More concisely: For any decidably equal type `α` and elements `a` in unordered pair `z` of type `Sym2 α`, `a` paired with the other element of `z` using `Sym2.Mem.other'` equals `z`.
|
Mathlib.Data.Sym.Sym2._auxLemma.1
theorem Mathlib.Data.Sym.Sym2._auxLemma.1 : ∀ {α : Type u_1} {p q : α × α}, Sym2.Rel α p q = (p = q ∨ p = q.swap) := by
sorry
This theorem named `Mathlib.Data.Sym.Sym2._auxLemma.1` states that for any type `α`, and for any pairs `p` and `q` of type α (denoted as `p : α × α` and `q : α × α`), the relation `Sym2.Rel α p q` holds if and only if either `p` is equal to `q` or `p` is equal to the swapped version of `q` (as defined by the `Prod.swap` function). In other words, two pairs are considered related under `Sym2.Rel` if they are identical or if one is the swapped version of the other.
More concisely: The theorem `Mathlib.Data.Sym.Sym2._auxLemma.1` in Lean 4 states that for any type `α`, the binary relation `Sym2.Rel α` on pairs of `α` is an equivalence relation, where two pairs `(p, q)` are related if and only if `p = q` or `p = Swap p q`.
|
Mathlib.Data.Sym.Sym2._auxLemma.17
theorem Mathlib.Data.Sym.Sym2._auxLemma.17 : ∀ {α : Type u_1} (z : α × α), (Sym2.mk z).IsDiag = (z.1 = z.2)
This theorem, `Mathlib.Data.Sym.Sym2._auxLemma.17`, states that for any type `α` and any pair `z` of type `α`, the predicate `Sym2.IsDiag` applied to the result of `Sym2.mk` applied to `z` is equivalent to checking if the two elements of `z` are equal. In other words, an element of the symmetric square of a type `α` is on the diagonal if and only if its two components are equal.
More concisely: For any type `α` and any pair `z` of elements of type `α`, the element `Sym2.mk z z` in the symmetric square of `α` is on the diagonal if and only if the components of `z` are equal.
|
Mathlib.Data.Sym.Sym2._auxLemma.20
theorem Mathlib.Data.Sym.Sym2._auxLemma.20 :
∀ {α : Type u_1} (s : Set (Sym2 α)) (x y : α), Sym2.ToRel s x y = (s(x, y) ∈ s)
This theorem states that for any type `α`, any set `s` of symmetric pairs of type `α`, and any elements `x` and `y` of type `α`, the property of `(x, y)` being in the symmetric relation derived from set `s` is equivalent to the pair `(x, y)` being a member of the set `s`. In simpler terms, it claims that the symmetric relation described by `Sym2.ToRel` for a particular set `s` of unordered pairs, is the same as the membership relation of the pairs in that set.
More concisely: For any set `s` of symmetric pairs of type `α`, the relation defined by `Sym2.ToRel` on type `α` is equal to the membership relation of `s`.
|
Sym2.inductionOn
theorem Sym2.inductionOn : ∀ {α : Type u_1} {f : Sym2 α → Prop} (i : Sym2 α), (∀ (x y : α), f s(x, y)) → f i
The theorem `Sym2.inductionOn` states that for any type `α`, a property `f` on the symmetric square of `α` (i.e., unordered pairs of elements from `α`), and an instance `i` of the symmetric square of `α`, if the property `f` holds for any pair of elements `(x, y)` from `α` (considered as an instance of the symmetric square `s(x, y)`), then the property `f` also holds for the instance `i`. This theorem provides the basis for induction on instances of the symmetric square of a type.
More concisely: If a binary property holds for all unordered pairs of elements in a type, then it holds for any symmetric square instance.
|
Sym2.mem_mk_left
theorem Sym2.mem_mk_left : ∀ {α : Type u_1} (x y : α), x ∈ s(x, y)
This theorem, `Sym2.mem_mk_left`, states that for any type `α` and any pair of elements `x` and `y` from this type, `x` is a member of the two-element set that is formed by `x` and `y`. In other words, for every `x` and `y`, `x` is in the symmetric pair `(x, y)`.
More concisely: For any type `α` and any `x, y : α`, the pair `(x, y)` is a two-element set containing `x`.
|
Mathlib.Data.Sym.Sym2._auxLemma.2
theorem Mathlib.Data.Sym.Sym2._auxLemma.2 :
∀ {α : Type u_1} {p p' : α × α}, (Sym2.mk p = Sym2.mk p') = Sym2.Rel α p p'
This theorem states that for any type `α` and any two pairs of elements `p` and `p'` of type `α`, the statement "the symmetric product of `p` is equal to the symmetric product of `p'`" is equivalent to "the symmetric relation `Sym2.Rel` holds between `p` and `p'`". Here, `Sym2.mk` is a function that maps a pair of elements to their symmetric product, and `Sym2.Rel` is a relation that describes when two pairs are considered "equivalent" in the context of symmetric products.
More concisely: The theorem asserts that for any type `α`, the symmetric products of `p` and `p'` are equal if and only if `(p, p')` and `(p', p)` are related by `Sym2.Rel`.
|
Sym2.mem_iff
theorem Sym2.mem_iff : ∀ {α : Type u_1} {a b c : α}, a ∈ s(b, c) ↔ a = b ∨ a = c
This theorem states that for any type `α` and any elements `a`, `b`, and `c` of that type, `a` is a member of the symmetric pair formed by `b` and `c` (denoted as `s(b, c)`) if and only if `a` is equal to `b` or `a` is equal to `c`. In other words, an element belongs to a symmetric pair if it is one of the elements forming the pair.
More concisely: For any type `α` and elements `a`, `b`, `c` of `α`, `a` is in the symmetric pair `s(b, c)` if and only if `a = b` or `a = c`.
|