Documentation

Mathlib.Topology.Algebra.Star

Continuity of star #

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

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

Basic hypothesis to talk about a topological space with a continuous star operator.

Instances
    theorem ContinuousStar.continuous_star {R : Type u_1} :
    ∀ {inst : TopologicalSpace R} {inst_1 : 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} :
    theorem continuousWithinAt_star {R : Type u_2} [TopologicalSpace R] [Star R] [ContinuousStar R] {s : Set R} {x : R} :
    theorem continuousAt_star {R : Type u_2} [TopologicalSpace R] [Star R] [ContinuousStar R] {x : R} :
    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]
    theorem starContinuousMap_apply {R : Type u_2} [TopologicalSpace R] [Star R] [ContinuousStar R] :
    ∀ (a : R), starContinuousMap a = star a

    The star operation bundled as a continuous map.

    Equations
    • starContinuousMap = { toFun := star, continuous_toFun := }
    Instances For
      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
      • =