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 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⋆)⁻¹⋆)⁻¹⁻¹

def Set.star {α : Type u_1} [inst : Star α] :

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

Equations

Set.star = { star := Set.preimage star }

@[simp]

theorem Set.star_empty {α : Type u_1} [inst : Star α] :

@[simp]

theorem Set.star_univ {α : Type u_1} [inst : Star α] :

star Set.univ = Set.univ

@[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]

theorem Set.mem_star {α : Type u_1} {s : Set α} {a : α} [inst : Star α] :

a ∈ star s ↔ star a ∈ s

theorem Set.star_mem_star {α : Type u_1} {s : Set α} {a : α} [inst : InvolutiveStar α] :

star a ∈ star s ↔ a ∈ s

@[simp]

theorem Set.star_preimage {α : Type u_1} {s : Set α} [inst : Star α] :

star ⁻¹' s = star s

@[simp]

theorem Set.image_star {α : Type u_1} {s : Set α} [inst : InvolutiveStar α] :

star '' s = star s

@[simp]

theorem Set.inter_star {α : Type u_1} {s : Set α} {t : Set α} [inst : Star α] :

star (s ∩ t) = star s ∩ star t

@[simp]

theorem Set.union_star {α : Type u_1} {s : Set α} {t : Set α} [inst : Star α] :

star (s ∪ t) = star s ∪ star t

@[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)

@[simp]

theorem Set.compl_star {α : Type u_1} {s : Set α} [inst : Star α] :

star (sᶜ) = star sᶜ

noncomputable instance Set.instInvolutiveStarSet {α : Type u_1} [inst : InvolutiveStar α] :

InvolutiveStar (Set α)

Equations

Set.instInvolutiveStarSet = InvolutiveStar.mk (_ : ∀ (s : Set α), (fun x => star (star x)) ⁻¹' s = s)

@[simp]

theorem Set.star_subset_star {α : Type u_1} [inst : InvolutiveStar α] {s : Set α} {t : Set α} :

star s ⊆ star t ↔ s ⊆ t

theorem Set.star_subset {α : Type u_1} [inst : InvolutiveStar α] {s : Set α} {t : Set α} :

star s ⊆ t ↔ s ⊆ star t

theorem Set.Finite.star {α : Type u_1} [inst : InvolutiveStar α] {s : Set α} (hs : Set.Finite s) :

Set.Finite (star s)

theorem Set.star_singleton {β : Type u_1} [inst : InvolutiveStar β] (x : β) :

star {x} = {star x}

theorem Set.star_mul {α : Type u_1} [inst : Monoid α] [inst : StarSemigroup α] (s : Set α) (t : Set α) :

star (s * t) = star t * star s

theorem Set.star_add {α : Type u_1} [inst : AddMonoid α] [inst : StarAddMonoid α] (s : Set α) (t : Set α) :

star (s + t) = star s + star t

@[simp]

instance Set.instTrivialStarSetStar {α : Type u_1} [inst : Star α] [inst : TrivialStar α] :

TrivialStar (Set α)

Equations

@Set.instTrivialStarSetStar = @Set.instTrivialStarSetStar.proof_1

theorem Set.star_inv {α : Type u_1} [inst : Group α] [inst : StarSemigroup α] (s : Set α) :

star s⁻¹ = (star s)⁻¹

theorem Set.star_inv' {α : Type u_1} [inst : DivisionRing α] [inst : StarRing α] (s : Set α) :

star s⁻¹ = (star s)⁻¹