# Continuity of star#

This file defines the ContinuousStar typeclass, along with instances on Pi, Prod, MulOpposite, and Units.

class ContinuousStar (R : Type u_1) [] [Star R] :

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} [] [Star R] [self : ] :

The star operator is continuous.

theorem continuousOn_star {R : Type u_2} [] [Star R] [] {s : Set R} :
theorem continuousWithinAt_star {R : Type u_2} [] [Star R] [] {s : Set R} {x : R} :
theorem continuousAt_star {R : Type u_2} [] [Star R] [] {x : R} :
theorem tendsto_star {R : Type u_2} [] [Star R] [] (a : R) :
Filter.Tendsto star (nhds a) (nhds (star a))
theorem Filter.Tendsto.star {α : Type u_1} {R : Type u_2} [] [Star R] [] {f : αR} {l : } {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} [] [Star R] [] [] {f : αR} (hf : ) :
Continuous fun (x : α) => star (f x)
theorem ContinuousAt.star {α : Type u_1} {R : Type u_2} [] [Star R] [] [] {f : αR} {x : α} (hf : ) :
ContinuousAt (fun (x : α) => star (f x)) x
theorem ContinuousOn.star {α : Type u_1} {R : Type u_2} [] [Star R] [] [] {f : αR} {s : Set α} (hf : ) :
ContinuousOn (fun (x : α) => star (f x)) s
theorem ContinuousWithinAt.star {α : Type u_1} {R : Type u_2} [] [Star R] [] [] {f : αR} {s : Set α} {x : α} (hf : ) :
ContinuousWithinAt (fun (x : α) => star (f x)) s x
@[simp]
theorem starContinuousMap_apply {R : Type u_2} [] [Star R] [] :
∀ (a : R), starContinuousMap a = star a
def starContinuousMap {R : Type u_2} [] [Star R] [] :
C(R, R)

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] [] [] [] [] :
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] [] [] :
Equations
• =
instance instContinuousStarUnits {R : Type u_1} [] [] [] [] :
Equations
• =