Pointwise star operation on sets #
This file defines the star operation pointwise on sets and provides the basic API.
Besides basic facts about about how the star operation acts on sets (e.g., (s ∩ t)⋆ = s⋆ ∩ t⋆∩ t)⋆ = s⋆ ∩ t⋆⋆ = s⋆ ∩ t⋆⋆ ∩ t⋆∩ t⋆⋆
),
if s t : Set α
, then under suitable assumption on α
, it is shown
(s + t)⋆ = s⋆ + t⋆⋆ = s⋆ + t⋆⋆ + t⋆⋆
(s * t)⋆ = t⋆ + s⋆⋆ = t⋆ + s⋆⋆ + s⋆⋆
(s⁻¹)⋆ = (s⋆)⁻¹⁻¹)⋆ = (s⋆)⁻¹⋆ = (s⋆)⁻¹⋆)⁻¹⁻¹
@[simp]
theorem
Set.nonempty_star
{α : Type u_1}
[inst : InvolutiveStar α]
{s : Set α}
:
Set.Nonempty (star s) ↔ Set.Nonempty s
theorem
Set.Nonempty.star
{α : Type u_1}
[inst : InvolutiveStar α]
{s : Set α}
(h : Set.Nonempty s)
:
Set.Nonempty (star s)
@[simp]
@[simp]
theorem
Set.interᵢ_star
{α : Type u_2}
{ι : Sort u_1}
[inst : Star α]
(s : ι → Set α)
:
star (Set.interᵢ fun i => s i) = Set.interᵢ fun i => star (s i)
@[simp]
theorem
Set.unionᵢ_star
{α : Type u_2}
{ι : Sort u_1}
[inst : Star α]
(s : ι → Set α)
:
star (Set.unionᵢ fun i => s i) = Set.unionᵢ fun i => star (s i)
noncomputable instance
Set.instInvolutiveStarSet
{α : Type u_1}
[inst : InvolutiveStar α]
:
InvolutiveStar (Set α)
theorem
Set.Finite.star
{α : Type u_1}
[inst : InvolutiveStar α]
{s : Set α}
(hs : Set.Finite s)
:
Set.Finite (star s)
@[simp]
instance
Set.instTrivialStarSetStar
{α : Type u_1}
[inst : Star α]
[inst : TrivialStar α]
:
TrivialStar (Set α)