Mathlib.Algebra.Star.Pointwise

Set.star definition

[Star α] : Star (Set α)

Full source

/-- 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`. -/
protected def star [Star α] : Star (Set α) := ⟨preimage Star.star⟩

Star operation on sets

Informal description

Given a type $\alpha$ equipped with a star operation (involution), the star operation on a set $s \subseteq \alpha$ is defined as the preimage of $s$ under the star operation, i.e., $\{x \in \alpha \mid x^* \in s\}$. In the case where the star operation is involutive, this is equivalent to $\{x^* \mid x \in s\}$.

Set.star_empty theorem

[Star α] : (∅ : Set α)⋆ = ∅

Full source

@[simp]
theorem star_empty [Star α] : (∅ : Set α)⋆ = ∅ := rfl

Star of Empty Set is Empty

Informal description

For any type $\alpha$ equipped with a star operation, the star of the empty set is the empty set, i.e., $\emptyset^\star = \emptyset$.

Set.star_univ theorem

[Star α] : (univ : Set α)⋆ = univ

Full source

@[simp]
theorem star_univ [Star α] : (univ : Set α)⋆ = univ := rfl

Star Operation Preserves Universal Set: $\text{univ}^\star = \text{univ}$

Informal description

For any type $\alpha$ equipped with a star operation, the star operation applied to the universal set $\text{univ} \subseteq \alpha$ yields the universal set again, i.e., $\text{univ}^\star = \text{univ}$.

Set.nonempty_star theorem

[InvolutiveStar α] {s : Set α} : s⋆.Nonempty ↔ s.Nonempty

Full source

@[simp]
theorem nonempty_star [InvolutiveStar α] {s : Set α} : s⋆s⋆.Nonempty ↔ s.Nonempty :=
  star_involutive.surjective.nonempty_preimage

Nonempty Characterization of Starred Sets: $s^\star \neq \emptyset \iff s \neq \emptyset$

Informal description

Let $\alpha$ be a type equipped with an involutive star operation $\star$. For any subset $s \subseteq \alpha$, the starred set $s^\star$ is nonempty if and only if $s$ is nonempty. In symbols: \[ s^\star \neq \emptyset \iff s \neq \emptyset. \]

Set.Nonempty.star theorem

[InvolutiveStar α] {s : Set α} (h : s.Nonempty) : s⋆.Nonempty

Full source

theorem Nonempty.star [InvolutiveStar α] {s : Set α} (h : s.Nonempty) : s⋆.Nonempty :=
  nonempty_star.2 h

Nonempty Sets Preserved Under Star Operation

Informal description

Let $\alpha$ be a type equipped with an involutive star operation $\star$. For any nonempty subset $s \subseteq \alpha$, the starred set $s^\star$ is also nonempty.

Set.mem_star theorem

[Star α] : a ∈ s⋆ ↔ a⋆ ∈ s

Full source

@[simp]
theorem mem_star [Star α] : a ∈ s⋆a ∈ s⋆ ↔ a⋆ ∈ s := Iff.rfl

Characterization of Membership in Starred Set

Informal description

For any element $a$ in a type $\alpha$ equipped with a star operation and any subset $s$ of $\alpha$, the element $a$ belongs to the star of $s$ if and only if the star of $a$ belongs to $s$. In symbols: \[ a \in s^\star \leftrightarrow a^\star \in s. \]

Set.star_mem_star theorem

[InvolutiveStar α] : a⋆ ∈ s⋆ ↔ a ∈ s

Full source

theorem star_mem_star [InvolutiveStar α] : a⋆a⋆ ∈ s⋆a⋆ ∈ s⋆ ↔ a ∈ s := by simp only [mem_star, star_star]

Star Membership Equivalence: $a^\star \in s^\star \leftrightarrow a \in s$

Informal description

For any element $a$ in a type $\alpha$ equipped with an involutive star operation $\star$, and for any subset $s \subseteq \alpha$, the star of $a$ belongs to the star of $s$ if and only if $a$ belongs to $s$. In other words, $a^\star \in s^\star \leftrightarrow a \in s$.

Set.star_preimage theorem

[Star α] : Star.star ⁻¹' s = s⋆

Full source

@[simp]
theorem star_preimage [Star α] : Star.starStar.star ⁻¹' s = s⋆ := rfl

Preimage of Star Operation Equals Star of Set

Informal description

For any set $s$ in a type $\alpha$ equipped with a star operation, the preimage of $s$ under the star operation is equal to the star of $s$, i.e., $\text{Star.star}^{-1}(s) = s^\star$.

Set.image_star theorem

[InvolutiveStar α] : Star.star '' s = s⋆

Full source

@[simp]
theorem image_star [InvolutiveStar α] : Star.starStar.star '' s = s⋆ := by
  simp only [← star_preimage]
  rw [image_eq_preimage_of_inverse] <;> intro <;> simp only [star_star]

Image of Set under Star Operation Equals Star of Set

Informal description

For any set $s$ in a type $\alpha$ equipped with an involutive star operation $\star$, the image of $s$ under the star operation equals the star of $s$, i.e., $$\star(s) = s^\star.$$

Set.inter_star theorem

[Star α] : (s ∩ t)⋆ = s⋆ ∩ t⋆

Full source

@[simp]
theorem inter_star [Star α] : (s ∩ t)⋆ = s⋆s⋆ ∩ t⋆ := preimage_inter

Star Operation Preserves Intersection: $(s \cap t)^\star = s^\star \cap t^\star$

Informal description

For any type $\alpha$ equipped with a star operation and any subsets $s, t \subseteq \alpha$, the star of their intersection equals the intersection of their stars: $$ (s \cap t)^\star = s^\star \cap t^\star $$

Set.union_star theorem

[Star α] : (s ∪ t)⋆ = s⋆ ∪ t⋆

Full source

@[simp]
theorem union_star [Star α] : (s ∪ t)⋆ = s⋆s⋆ ∪ t⋆ := preimage_union

Star Operation Preserves Union of Sets

Informal description

For any type $\alpha$ equipped with a star operation and any subsets $s, t \subseteq \alpha$, the star of their union equals the union of their stars, i.e., $$(s \cup t)^\star = s^\star \cup t^\star.$$

Set.iInter_star theorem

{ι : Sort*} [Star α] (s : ι → Set α) : (⋂ i, s i)⋆ = ⋂ i, (s i)⋆

Full source

@[simp]
theorem iInter_star {ι : Sort*} [Star α] (s : ι → Set α) : (⋂ i, s i)⋆ = ⋂ i, (s i)⋆ :=
  preimage_iInter

Star Operation Preserves Intersection of Sets

Informal description

Let $\alpha$ be a type equipped with a star operation (involution). For any family of sets $\{s_i\}_{i \in \iota}$ in $\alpha$, the star of their intersection equals the intersection of their stars: \[ \left(\bigcap_{i} s_i\right)^\star = \bigcap_{i} (s_i)^\star. \]

Set.iUnion_star theorem

{ι : Sort*} [Star α] (s : ι → Set α) : (⋃ i, s i)⋆ = ⋃ i, (s i)⋆

Full source

@[simp]
theorem iUnion_star {ι : Sort*} [Star α] (s : ι → Set α) : (⋃ i, s i)⋆ = ⋃ i, (s i)⋆ :=
  preimage_iUnion

Star Operation Commutes with Union of Sets

Informal description

For any indexed family of sets $\{s_i\}_{i \in \iota}$ in a type $\alpha$ equipped with a star operation, the star of their union equals the union of their stars. In symbols: $$ \left(\bigcup_{i} s_i\right)^\star = \bigcup_{i} s_i^\star $$

Set.compl_star theorem

[Star α] : sᶜ⋆ = s⋆ᶜ

Full source

@[simp]
theorem compl_star [Star α] : sᶜsᶜ⋆ = s⋆s⋆ᶜ := preimage_compl

Star of Complement Equals Complement of Star

Informal description

For any set $s$ in a type $\alpha$ equipped with a star operation, the star of the complement of $s$ is equal to the complement of the star of $s$, i.e., $(s^c)^\star = (s^\star)^c$.

Set.instInvolutiveStar instance

[InvolutiveStar α] : InvolutiveStar (Set α)

Full source

@[simp]
instance [InvolutiveStar α] : InvolutiveStar (Set α) where
  star := Star.star
  star_involutive s := by simp only [← star_preimage, preimage_preimage, star_star, preimage_id']

Involutive Star Operation on Sets

Informal description

For any type $\alpha$ equipped with an involutive star operation, the collection of subsets of $\alpha$ inherits an involutive star operation, where the star of a set $s \subseteq \alpha$ is defined as $\{x^* \mid x \in s\}$.

Set.star_subset_star theorem

[InvolutiveStar α] {s t : Set α} : s⋆ ⊆ t⋆ ↔ s ⊆ t

Full source

@[simp]
theorem star_subset_star [InvolutiveStar α] {s t : Set α} : s⋆s⋆ ⊆ t⋆s⋆ ⊆ t⋆ ↔ s ⊆ t :=
  Equiv.star.surjective.preimage_subset_preimage_iff

Star Operation Preserves Subset Relation: $s^\star \subseteq t^\star \leftrightarrow s \subseteq t$

Informal description

Let $\alpha$ be a type equipped with an involutive star operation $\star$. For any subsets $s, t \subseteq \alpha$, the star of $s$ is contained in the star of $t$ if and only if $s$ is contained in $t$, i.e., $$ s^\star \subseteq t^\star \leftrightarrow s \subseteq t. $$

Set.star_subset theorem

[InvolutiveStar α] {s t : Set α} : s⋆ ⊆ t ↔ s ⊆ t⋆

Full source

theorem star_subset [InvolutiveStar α] {s t : Set α} : s⋆s⋆ ⊆ ts⋆ ⊆ t ↔ s ⊆ t⋆ := by
  rw [← star_subset_star, star_star]

Star Operation and Subset Relation: $s^\star \subseteq t \leftrightarrow s \subseteq t^\star$

Informal description

Let $\alpha$ be a type equipped with an involutive star operation $\star$. For any subsets $s, t \subseteq \alpha$, the star of $s$ is contained in $t$ if and only if $s$ is contained in the star of $t$, i.e., $$ s^\star \subseteq t \leftrightarrow s \subseteq t^\star. $$

Set.Finite.star theorem

[InvolutiveStar α] {s : Set α} (hs : s.Finite) : s⋆.Finite

Full source

theorem Finite.star [InvolutiveStar α] {s : Set α} (hs : s.Finite) : s⋆.Finite :=
  hs.preimage star_injective.injOn

Finite sets are preserved under the star operation

Informal description

For any set $s$ in a type $\alpha$ equipped with an involutive star operation $\star$, if $s$ is finite, then the star of $s$ (defined as $\{x^\star \mid x \in s\}$) is also finite.

Set.star_singleton theorem

{β : Type*} [InvolutiveStar β] (x : β) : ({ x } : Set β)⋆ = {x⋆}

Full source

theorem star_singleton {β : Type*} [InvolutiveStar β] (x : β) : ({x} : Set β)⋆ = {x⋆} := by
  ext1 y
  rw [mem_star, mem_singleton_iff, mem_singleton_iff, star_eq_iff_star_eq, eq_comm]

Star of Singleton Set: $\{x\}^\star = \{x^\star\}$

Informal description

For any element $x$ in a type $\beta$ equipped with an involutive star operation $\star$, the star of the singleton set $\{x\}$ is equal to the singleton set $\{x^\star\}$. In symbols: \[ \{x\}^\star = \{x^\star\}. \]

Set.star_mul theorem

[Mul α] [StarMul α] (s t : Set α) : (s * t)⋆ = t⋆ * s⋆

Full source

protected theorem star_mul [Mul α] [StarMul α] (s t : Set α) : (s * t)⋆ = t⋆ * s⋆ := by
 simp_rw [← image_star, ← image2_mul, image_image2, image2_image_left, image2_image_right,
   star_mul, image2_swap _ s t]

Star of Product of Sets: $(s \cdot t)^\star = t^\star \cdot s^\star$

Informal description

Let $\alpha$ be a type equipped with a multiplication operation and a star operation satisfying the *-magma property (i.e., $(r \cdot s)^\star = s^\star \cdot r^\star$ for all $r, s \in \alpha$). For any subsets $s, t \subseteq \alpha$, the star of their pointwise product equals the pointwise product of the stars of $t$ and $s$: $$(s \cdot t)^\star = t^\star \cdot s^\star.$$

Set.star_add theorem

[AddMonoid α] [StarAddMonoid α] (s t : Set α) : (s + t)⋆ = s⋆ + t⋆

Full source

protected theorem star_add [AddMonoid α] [StarAddMonoid α] (s t : Set α) : (s + t)⋆ = s⋆ + t⋆ := by
 simp_rw [← image_star, ← image2_add, image_image2, image2_image_left, image2_image_right,
   star_add]

Star Operation Preserves Addition of Sets: $(s + t)^\star = s^\star + t^\star$

Informal description

Let $\alpha$ be an additive monoid equipped with a star operation that is additive (i.e., $(a + b)^\star = a^\star + b^\star$ for all $a, b \in \alpha$). For any subsets $s, t \subseteq \alpha$, the star of their sum is equal to the sum of their stars: \[ (s + t)^\star = s^\star + t^\star. \]

Set.instTrivialStar instance

[Star α] [TrivialStar α] : TrivialStar (Set α)

Full source

@[simp]
instance [Star α] [TrivialStar α] : TrivialStar (Set α) where
  star_trivial s := by
    rw [← star_preimage]
    ext1
    simp [star_trivial]

Trivial Star Operation on Sets

Informal description

For any type $\alpha$ equipped with a star operation that is trivial (i.e., $\star r = r$ for all $r \in \alpha$), the star operation on sets of $\alpha$ is also trivial. This means that for any set $s \subseteq \alpha$, the star operation $s^\star$ is equal to $s$.

Set.star_inv theorem

[Group α] [StarMul α] (s : Set α) : s⁻¹⋆ = s⋆⁻¹

Full source

protected theorem star_inv [Group α] [StarMul α] (s : Set α) : s⁻¹s⁻¹⋆ = s⋆s⋆⁻¹ := by
  ext
  simp only [mem_star, mem_inv, star_inv]

Star Operation Preserves Pointwise Inversion in Groups: $(s^{-1})^\star = (s^\star)^{-1}$

Informal description

Let $\alpha$ be a group equipped with a star operation satisfying the *-magma property. For any subset $s \subseteq \alpha$, the star of the pointwise inverse of $s$ is equal to the pointwise inverse of the star of $s$, i.e., \[ (s^{-1})^\star = (s^\star)^{-1}. \]

Set.star_inv' theorem

[GroupWithZero α] [StarMul α] (s : Set α) : s⁻¹⋆ = s⋆⁻¹

Full source

protected theorem star_inv' [GroupWithZero α] [StarMul α] (s : Set α) : s⁻¹s⁻¹⋆ = s⋆s⋆⁻¹ := by
  ext
  simp only [mem_star, mem_inv, star_inv₀]

Star Operation Commutes with Set Inversion in Groups with Zero: $(s^{-1})^\star = (s^\star)^{-1}$

Informal description

Let $\alpha$ be a group with zero equipped with a star multiplication operation. For any subset $s \subseteq \alpha$, the star of the inverse of $s$ is equal to the inverse of the star of $s$, i.e., $(s^{-1})^\star = (s^\star)^{-1}$.

StarMemClass.star_coe_eq theorem

{S α : Type*} [InvolutiveStar α] [SetLike S α] [StarMemClass S α] (s : S) : star (s : Set α) = s

Full source

@[simp]
lemma StarMemClass.star_coe_eq {S α : Type*} [InvolutiveStar α] [SetLike S α]
    [StarMemClass S α] (s : S) : star (s : Set α) = s := by
  ext x
  simp only [Set.mem_star, SetLike.mem_coe]
  exact ⟨by simpa only [star_star] using star_mem (s := s) (r := star x), star_mem⟩

Star-closed Sets are Fixed under Star Operation

Informal description

Let $S$ be a set-like structure over a type $\alpha$ equipped with an involutive star operation, and suppose $S$ is closed under the star operation (i.e., for any $x \in s$ with $s \in S$, we have $x^* \in s$). Then, for any $s \in S$, the star of the set $s$ (viewed as a subset of $\alpha$) is equal to $s$ itself, i.e., $\{x^* \mid x \in s\} = s$.