English
For any set s in α with a Star α, the star on sets is defined by s⋆ = { x | star x ∈ s }. In particular, s⋆ is the preimage of s under star.
Русский
Для множества s в α с операцией звезды над α звезда множества определяется как s⋆ = { x | star x ∈ s }. Это является прообразом множества s под действием звезды.
LaTeX
$$$s^{\\star} = \\{ x \\mid \\ star\\ x \\in s \\}.$$$
Lean4
/-- The set `(star s : Set α)` is defined as `{x | star x ∈ s}` in the scope Pointwise`.
In the usual case where `star` is involutive, it is equal to `{star s | x ∈ s}`, see
`Set.image_star`. -/
protected def star [Star α] : Star (Set α) :=
⟨preimage Star.star⟩
