Mathlib.Topology.Algebra.Star

ContinuousStar structure

(R : Type*) [TopologicalSpace R] [Star R]

Full source

/-- Basic hypothesis to talk about a topological space with a continuous `star` operator. -/
class ContinuousStar (R : Type*) [TopologicalSpace R] [Star R] : Prop where
  /-- The `star` operator is continuous. -/
  continuous_star : Continuous (star : R → R)

Topological space with continuous star operation

Informal description

A topological space $R$ equipped with a continuous star operation $\star : R \to R$.

continuousOn_star theorem

{s : Set R} : ContinuousOn star s

Full source

theorem continuousOn_star {s : Set R} : ContinuousOn star s :=
  continuous_star.continuousOn

Continuity of Star Operation on Subsets

Informal description

For any subset $s$ of a topological space $R$ equipped with a star operation $\star$, the star operation is continuous on $s$.

continuousWithinAt_star theorem

{s : Set R} {x : R} : ContinuousWithinAt star s x

Full source

theorem continuousWithinAt_star {s : Set R} {x : R} : ContinuousWithinAt star s x :=
  continuous_star.continuousWithinAt

Continuity of Star Operation Within a Subset at a Point

Informal description

For any subset $s$ of a topological space $R$ with a star operation and any point $x \in R$, the star operation $\star$ is continuous within $s$ at $x$.

continuousAt_star theorem

{x : R} : ContinuousAt star x

Full source

theorem continuousAt_star {x : R} : ContinuousAt star x :=
  continuous_star.continuousAt

Continuity of Star Operation at a Point

Informal description

For any element $x$ in a topological space $R$ with a star operation, the star operation is continuous at $x$.

tendsto_star theorem

(a : R) : Tendsto star (𝓝 a) (𝓝 (star a))

Full source

theorem tendsto_star (a : R) : Tendsto star (𝓝 a) (𝓝 (star a)) :=
  continuousAt_star

Star Operation Preserves Limits at a Point

Informal description

For any element $a$ in a topological space $R$ with a star operation, the star operation $\star$ satisfies the limit condition that as $x$ approaches $a$, $\star(x)$ approaches $\star(a)$. In other words, the star operation preserves limits at $a$.

Filter.Tendsto.star theorem

{f : α → R} {l : Filter α} {y : R} (h : Tendsto f l (𝓝 y)) : Tendsto (fun x => star (f x)) l (𝓝 (star y))

Full source

theorem Filter.Tendsto.star {f : α → R} {l : Filter α} {y : R} (h : Tendsto f l (𝓝 y)) :
    Tendsto (fun x => star (f x)) l (𝓝 (star y)) :=
  (continuous_star.tendsto y).comp h

Star Operation Preserves Filter Limits

Informal description

Let $f : \alpha \to R$ be a function from a type $\alpha$ to a topological space $R$ with a continuous star operation, and let $l$ be a filter on $\alpha$. If $f$ tends to $y$ along $l$, then the function $x \mapsto \star(f(x))$ tends to $\star(y)$ along $l$.

Continuous.star theorem

(hf : Continuous f) : Continuous fun x => star (f x)

Full source

@[continuity, fun_prop]
theorem Continuous.star (hf : Continuous f) : Continuous fun x => star (f x) :=
  continuous_star.comp hf

Continuity of star operation under continuous functions

Informal description

Let $f$ be a continuous function from a topological space to a space $R$ with a continuous star operation. Then the function $x \mapsto \star(f(x))$ is also continuous.

ContinuousAt.star theorem

(hf : ContinuousAt f x) : ContinuousAt (fun x => star (f x)) x

Full source

@[fun_prop]
theorem ContinuousAt.star (hf : ContinuousAt f x) : ContinuousAt (fun x => star (f x)) x :=
  continuousAt_star.comp hf

Continuity of Star Operation under Continuous Functions at a Point

Informal description

If a function $f$ is continuous at a point $x$ in a topological space, then the function $x \mapsto \star(f(x))$ is also continuous at $x$.

ContinuousOn.star theorem

(hf : ContinuousOn f s) : ContinuousOn (fun x => star (f x)) s

Full source

@[fun_prop]
theorem ContinuousOn.star (hf : ContinuousOn f s) : ContinuousOn (fun x => star (f x)) s :=
  continuous_star.comp_continuousOn hf

Continuity of star operation under continuous functions on subsets

Informal description

Let $f$ be a function from a topological space to a space with a continuous star operation. If $f$ is continuous on a subset $s$, then the function $x \mapsto \star(f(x))$ is also continuous on $s$.

ContinuousWithinAt.star theorem

(hf : ContinuousWithinAt f s x) : ContinuousWithinAt (fun x => star (f x)) s x

Full source

theorem ContinuousWithinAt.star (hf : ContinuousWithinAt f s x) :
    ContinuousWithinAt (fun x => star (f x)) s x :=
  Filter.Tendsto.star hf

Continuity of Star Operation under Functions Continuous Within a Subset at a Point

Informal description

Let $f$ be a function from a topological space to a space with a continuous star operation. If $f$ is continuous within a subset $s$ at a point $x$, then the function $x \mapsto \star(f(x))$ is also continuous within $s$ at $x$.

starContinuousMap definition

: C(R, R)

Full source

/-- The star operation bundled as a continuous map. -/
@[simps]
def starContinuousMap : C(R, R) :=
  ⟨star, continuous_star⟩

Continuous star map

Informal description

The star operation $\star : R \to R$ bundled as a continuous map.

instContinuousStarProd instance

 [Star R] [Star S] [TopologicalSpace R] [TopologicalSpace S] [ContinuousStar R] [ContinuousStar S] :
  ContinuousStar (R × S)

Full source

instance [Star R] [Star S] [TopologicalSpace R] [TopologicalSpace S] [ContinuousStar R]
    [ContinuousStar S] : ContinuousStar (R × S) :=
  ⟨(continuous_star.comp continuous_fst).prodMk (continuous_star.comp continuous_snd)⟩

Continuous Star Operation on Product Spaces

Informal description

For any topological spaces $R$ and $S$ equipped with star operations, if the star operations on $R$ and $S$ are continuous, then the product space $R \times S$ also has a continuous star operation.

instContinuousStarForall instance

 {C : ι → Type*} [∀ i, TopologicalSpace (C i)] [∀ i, Star (C i)] [∀ i, ContinuousStar (C i)] : ContinuousStar (∀ i, C i)

Full source

instance {C : ι → Type*} [∀ i, TopologicalSpace (C i)] [∀ i, Star (C i)]
    [∀ i, ContinuousStar (C i)] : ContinuousStar (∀ i, C i) where
  continuous_star := continuous_pi fun i => Continuous.star (continuous_apply i)

Continuous Star Operation on Product of Spaces

Informal description

For any family of topological spaces $C_i$ indexed by $i$, each equipped with a star operation, if each star operation is continuous, then the star operation on the product space $\prod_i C_i$ is also continuous.

instContinuousStarMulOpposite instance

[Star R] [TopologicalSpace R] [ContinuousStar R] : ContinuousStar Rᵐᵒᵖ

Full source

instance [Star R] [TopologicalSpace R] [ContinuousStar R] : ContinuousStar Rᵐᵒᵖ :=
  ⟨MulOpposite.continuous_op.comp <| MulOpposite.continuous_unop.star⟩

Continuous Star Operation on Opposite Monoid

Informal description

For any topological space $R$ with a continuous star operation $\star : R \to R$, the opposite monoid $R^{\text{op}}$ also has a continuous star operation.

instContinuousStarUnits instance

[Monoid R] [StarMul R] [TopologicalSpace R] [ContinuousStar R] : ContinuousStar Rˣ

Full source

instance [Monoid R] [StarMul R] [TopologicalSpace R] [ContinuousStar R] :
    ContinuousStar Rˣ :=
  ⟨continuous_induced_rng.2 Units.continuous_embedProduct.star⟩

Continuous Star Operation on the Group of Units

Informal description

For any monoid $R$ with a star operation $\star : R \to R$ that preserves multiplication, if $R$ is equipped with a topological space structure where the star operation is continuous, then the group of units $R^\times$ also has a continuous star operation.