Set.star_mem_star
theorem Set.star_mem_star : ∀ {α : Type u_1} {s : Set α} {a : α} [inst : InvolutiveStar α], star a ∈ star s ↔ a ∈ s
The theorem `Set.star_mem_star` states that for any type `α`, any set `s` of elements of type `α`, and any element `a` of type `α`, given that the operation `star` on `α` is involutive, the property `star a ∈ star s` is equivalent to `a ∈ s`. In other words, an element is in the set `s` if and only if its `star` image is in the `star` image of the set, under the condition that `star` is an operation that reverses itself when applied twice.
More concisely: For any set `s` and involutive operation `star` on a type `α`, an element `a` belongs to `s` if and only if its `star` image belongs to the `star` image of `s`.
|
Set.mem_star
theorem Set.mem_star : ∀ {α : Type u_1} {s : Set α} {a : α} [inst : Star α], a ∈ star s ↔ star a ∈ s
This theorem, `Set.mem_star`, states that for all types `α` and any set `s` of type `α` and any element `a` of the same type, given that `α` has a star operation, then `a` is in the star of `s` if and only if the star of `a` is in `s`. Here the "star" could be any unary operation that forms a semigroup or monoid on the type `α`. For example, in the case of strings, "star" could be the operation of reversing the string.
More concisely: For any type `α` with a star operation, and set `s` of type `α`, an element `a` is in the star of `s` if and only if the star of `a` is in `s`.
|
Mathlib.Algebra.Star.Pointwise._auxLemma.2
theorem Mathlib.Algebra.Star.Pointwise._auxLemma.2 :
∀ {α : Type u_1} {s : Set α} {a : α} [inst : Star α], (a ∈ star s) = (star a ∈ s)
The theorem `Mathlib.Algebra.Star.Pointwise._auxLemma.2` states that for any type `α`, any set `s` of `α`, and any element `a` of `α`, given that `Star` is defined for `α`, the property of `a` being in the star closure of `s` is equivalent to the star of `a` being in the set `s`. Here, the star operation typically means taking the adjoint in the context of star algebras.
More concisely: For any type `α`, set `s` of `α`, and element `a` of `α` in a star algebra, `a` is in the star closure of `s` if and only if the star of `a` is in `s`.
|