Mathlib.GroupTheory.DoubleCoset._auxLemma.4
theorem Mathlib.GroupTheory.DoubleCoset._auxLemma.4 :
∀ {α : Type u_2} [inst : Mul α] {s t : Set α} {a b : α},
(b ∈ Doset.doset a s t) = ∃ x ∈ s, ∃ y ∈ t, b = x * a * y
This theorem states that for any type `α` equipped with a multiplication operation, any two sets `s` and `t` of type `α`, and any two elements `a` and `b` of type `α`, the condition that `b` is in the double coset of `a` with respect to `s` and `t` is equivalent to the existence of an element `x` in `s` and an element `y` in `t` such that `b` is equal to the product of `x`, `a`, and `y` in that order. In mathematical terms, we could write the result as $b \in s \cdot \{a\} \cdot t \iff \exists x \in s, y \in t: b = x \cdot a \cdot y$.
More concisely: For any type `α` with multiplication, sets `s` and `t` of `α`, and elements `a`, `b` in `α`, `b` is in the double coset of `a` with respect to `s` and `t` if and only if there exist `x` in `s` and `y` in `t` such that `b = x * a * y`.
|
Doset.mem_doset
theorem Doset.mem_doset :
∀ {α : Type u_2} [inst : Mul α] {s t : Set α} {a b : α}, b ∈ Doset.doset a s t ↔ ∃ x ∈ s, ∃ y ∈ t, b = x * a * y
This theorem, `Doset.mem_doset`, states that for any given type `α` that supports multiplication, sets `s` and `t` of type `α`, and elements `a` and `b` of type `α`, `b` is an element of the double coset `Doset.doset a s t` if and only if there exist elements `x` in set `s` and `y` in set `t` such that `b` is equal to the product of `x`, `a`, and `y` (denoted as `b = x * a * y`). In essence, the theorem formalizes the condition for an element to belong to a double coset in terms of the element being a specific product of elements from the original sets and a fixed element.
More concisely: A element b belongs to the double coset Doset.doset a s t if and only if there exist x in s and y in t such that b = x * a * y.
|
Mathlib.GroupTheory.DoubleCoset._auxLemma.5
theorem Mathlib.GroupTheory.DoubleCoset._auxLemma.5 :
∀ {α : Type u} {ι : Sort v} {x : α} {s : ι → Set α}, (x ∈ ⋃ i, s i) = ∃ i, x ∈ s i
This theorem states that for any type `α`, any indexing type `ι`, any element `x` of type `α`, and any family of sets `s` indexed by `ι`, the membership of `x` in the union of all sets in the family `s` is equivalent to the existence of an index `i` such that `x` is a member of the set `s` at index `i`. In mathematical terms, this theorem states that $x \in \bigcup_{i} s_i$ if and only if there exists an $i$ such that $x \in s_i$.
More concisely: For any type `α`, indexing type `ι`, element `x` of type `α`, and set family `s` indexed by `ι`, `x` is in the union of `s` if and only if there exists an `i` such that `x` is in `s` at index `i`. In mathematical notation, this is expressed as `x ∈ ⋃i. si ↔ ∃i, x ∈ si`.
|
Mathlib.GroupTheory.DoubleCoset._auxLemma.10
theorem Mathlib.GroupTheory.DoubleCoset._auxLemma.10 :
∀ {G : Type u_1} [inst : Semigroup G] (a b c : G), a * (b * c) = a * b * c
This theorem, `Mathlib.GroupTheory.DoubleCoset._auxLemma.10`, states that for any semigroup `G` and any three elements `a`, `b`, and `c` of `G`, the operation `a * (b * c)` is equal to `a * b * c`. In other words, it asserts the associativity of the semigroup operation, meaning that the way in which operations are grouped does not change the result.
More concisely: For any semigroup G and all elements a, b, and c in G, the associative property holds, that is, a * (b * c) = a * b * c.
|