HepLean Documentation

Mathlib.Algebra.Star.Pointwise

Pointwise star operation on sets #

This file defines the star operation pointwise on sets and provides the basic API. Besides basic facts about how the star operation acts on sets (e.g., (s ∩ t)⋆ = s⋆ ∩ t⋆), if s t : Set α, then under suitable assumption on α, it is shown

source
def Set.star {α : Type u_1} [Star α] :
Star (Set α)

The set (star s : Set α) is defined as {x | star x ∈ s} in the locale Pointwise. In the usual case where star is involutive, it is equal to {star s | x ∈ s}, see Set.image_star.

Equations
Instances For
    source
    @[simp]
    theorem Set.star_empty {α : Type u_1} [Star α] :
    star ∅ = ∅
    source
    @[simp]
    theorem Set.star_univ {α : Type u_1} [Star α] :
    star Set.univ = Set.univ
    source
    @[simp]
    theorem Set.nonempty_star {α : Type u_1} [InvolutiveStar α] {s : Set α} :
    (star s).Nonempty ↔ s.Nonempty
    source
    theorem Set.Nonempty.star {α : Type u_1} [InvolutiveStar α] {s : Set α} (h : s.Nonempty) :
    (star s).Nonempty
    source
    @[simp]
    theorem Set.mem_star {α : Type u_1} {s : Set α} {a : α} [Star α] :
    a ∈ star s ↔ star a ∈ s
    source
    theorem Set.star_mem_star {α : Type u_1} {s : Set α} {a : α} [InvolutiveStar α] :
    star a ∈ star s ↔ a ∈ s
    source
    @[simp]
    theorem Set.star_preimage {α : Type u_1} {s : Set α} [Star α] :
    star ⁻¹' s = star s
    source
    @[simp]
    theorem Set.image_star {α : Type u_1} {s : Set α} [InvolutiveStar α] :
    star '' s = star s
    source
    @[simp]
    theorem Set.inter_star {α : Type u_1} {s : Set α} {t : Set α} [Star α] :
    star (s ∩ t) = star s ∩ star t
    source
    @[simp]
    theorem Set.union_star {α : Type u_1} {s : Set α} {t : Set α} [Star α] :
    star (s ∪ t) = star s ∪ star t
    source
    @[simp]
    theorem Set.iInter_star {α : Type u_1} {ι : Sort u_2} [Star α] (s : ι → Set α) :
    star (⋂ (i : ι), s i) = ⋂ (i : ι), star (s i)
    source
    @[simp]
    theorem Set.iUnion_star {α : Type u_1} {ι : Sort u_2} [Star α] (s : ι → Set α) :
    star (⋃ (i : ι), s i) = ⋃ (i : ι), star (s i)
    source
    @[simp]
    theorem Set.compl_star {α : Type u_1} {s : Set α} [Star α] :
    star sᶜ = (star s)ᶜ
    source
    instance Set.instInvolutiveStar {α : Type u_1} [InvolutiveStar α] :
    InvolutiveStar (Set α)
    Equations
    source
    @[simp]
    theorem Set.star_subset_star {α : Type u_1} [InvolutiveStar α] {s : Set α} {t : Set α} :
    star s ⊆ star t ↔ s ⊆ t
    source
    theorem Set.star_subset {α : Type u_1} [InvolutiveStar α] {s : Set α} {t : Set α} :
    star s ⊆ t ↔ s ⊆ star t
    source
    theorem Set.Finite.star {α : Type u_1} [InvolutiveStar α] {s : Set α} (hs : s.Finite) :
    (star s).Finite
    source
    theorem Set.star_singleton {β : Type u_2} [InvolutiveStar β] (x : β) :
    star {x} = {star x}
    source
    theorem Set.star_mul {α : Type u_1} [Mul α] [StarMul α] (s : Set α) (t : Set α) :
    star (s * t) = star t * star s
    source
    theorem Set.star_add {α : Type u_1} [AddMonoid α] [StarAddMonoid α] (s : Set α) (t : Set α) :
    star (s + t) = star s + star t
    source
    @[simp]
    instance Set.instTrivialStar {α : Type u_1} [Star α] [TrivialStar α] :
    TrivialStar (Set α)
    Equations
    • ⋯ = ⋯
    source
    theorem Set.star_inv {α : Type u_1} [Group α] [StarMul α] (s : Set α) :
    star s⁻¹ = (star s)⁻¹
    source
    theorem Set.star_inv' {α : Type u_1} [DivisionSemiring α] [StarRing α] (s : Set α) :
    star s⁻¹ = (star s)⁻¹
    source
    @[simp]
    theorem StarMemClass.star_coe_eq {S : Type u_1} {α : Type u_2} [InvolutiveStar α] [SetLike S α] [StarMemClass S α] (s : S) :
    star ↑s = ↑s