# Continuity of `star`

#

This file defines the `ContinuousStar`

typeclass, along with instances on `Pi`

, `Prod`

,
`MulOpposite`

, and `Units`

.

Basic hypothesis to talk about a topological space with a continuous `star`

operator.

- continuous_star : Continuous star
The

`star`

operator is continuous.

## Instances

theorem
ContinuousStar.continuous_star
{R : Type u_1}
[TopologicalSpace R]
[Star R]
[self : ContinuousStar R]
:

Continuous star

The `star`

operator is continuous.

theorem
continuousOn_star
{R : Type u_2}
[TopologicalSpace R]
[Star R]
[ContinuousStar R]
{s : Set R}
:

ContinuousOn star s

theorem
continuousWithinAt_star
{R : Type u_2}
[TopologicalSpace R]
[Star R]
[ContinuousStar R]
{s : Set R}
{x : R}
:

ContinuousWithinAt star s x

theorem
continuousAt_star
{R : Type u_2}
[TopologicalSpace R]
[Star R]
[ContinuousStar R]
{x : R}
:

ContinuousAt star x

theorem
tendsto_star
{R : Type u_2}
[TopologicalSpace R]
[Star R]
[ContinuousStar R]
(a : R)
:

Filter.Tendsto star (nhds a) (nhds (star a))

theorem
Filter.Tendsto.star
{α : Type u_1}
{R : Type u_2}
[TopologicalSpace R]
[Star R]
[ContinuousStar R]
{f : α → R}
{l : Filter α}
{y : R}
(h : Filter.Tendsto f l (nhds y))
:

Filter.Tendsto (fun (x : α) => star (f x)) l (nhds (star y))

theorem
Continuous.star
{α : Type u_1}
{R : Type u_2}
[TopologicalSpace R]
[Star R]
[ContinuousStar R]
[TopologicalSpace α]
{f : α → R}
(hf : Continuous f)
:

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

theorem
ContinuousAt.star
{α : Type u_1}
{R : Type u_2}
[TopologicalSpace R]
[Star R]
[ContinuousStar R]
[TopologicalSpace α]
{f : α → R}
{x : α}
(hf : ContinuousAt f x)
:

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

theorem
ContinuousOn.star
{α : Type u_1}
{R : Type u_2}
[TopologicalSpace R]
[Star R]
[ContinuousStar R]
[TopologicalSpace α]
{f : α → R}
{s : Set α}
(hf : ContinuousOn f s)
:

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

theorem
ContinuousWithinAt.star
{α : Type u_1}
{R : Type u_2}
[TopologicalSpace R]
[Star R]
[ContinuousStar R]
[TopologicalSpace α]
{f : α → R}
{s : Set α}
{x : α}
(hf : ContinuousWithinAt f s x)
:

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

@[simp]

The star operation bundled as a continuous map.

## Equations

- starContinuousMap = { toFun := star, continuous_toFun := ⋯ }

## Instances For

instance
instContinuousStarProd
{R : Type u_1}
{S : Type u_2}
[Star R]
[Star S]
[TopologicalSpace R]
[TopologicalSpace S]
[ContinuousStar R]
[ContinuousStar S]
:

ContinuousStar (R × S)

## Equations

- ⋯ = ⋯

instance
instContinuousStarForall
{ι : Type u_3}
{C : ι → Type u_4}
[(i : ι) → TopologicalSpace (C i)]
[(i : ι) → Star (C i)]
[∀ (i : ι), ContinuousStar (C i)]
:

ContinuousStar ((i : ι) → C i)

## Equations

- ⋯ = ⋯

instance
instContinuousStarMulOpposite
{R : Type u_1}
[Star R]
[TopologicalSpace R]
[ContinuousStar R]
:

## Equations

- ⋯ = ⋯

instance
instContinuousStarUnits
{R : Type u_1}
[Monoid R]
[StarMul R]
[TopologicalSpace R]
[ContinuousStar R]
:

## Equations

- ⋯ = ⋯