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.

continuous_star : Continuous star
The star operator is continuous.

Instances

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 : Tendsto f l (nhds y)) :

Tendsto (fun (x : α) => Star.star (f x)) l (nhds (Star.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 (Star.star f)

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

Continuous fun (i : α) => Star.star (f i)

Eta-expanded form of Continuous.star

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 (Star.star f) x

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

ContinuousAt (fun (i : α) => Star.star (f i)) x

Eta-expanded form of ContinuousAt.star

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 (Star.star f) s

theorem ContinuousOn.fun_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 (i : α) => Star.star (f i)) s

Eta-expanded form of ContinuousOn.star

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 (Star.star f) s x

theorem ContinuousWithinAt.fun_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 (i : α) => Star.star (f i)) s x

Eta-expanded form of ContinuousWithinAt.star

def starContinuousMap {R : Type u_2} [TopologicalSpace R] [Star R] [ContinuousStar R] :

The star operation bundled as a continuous map.

Equations

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

Instances For

@[simp]

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

starContinuousMap a✝ = star a✝

@[simp]

theorem continuous_star_iff {α : Type u_1} {R : Type u_2} [TopologicalSpace R] [InvolutiveStar R] [ContinuousStar R] [TopologicalSpace α] {f : α → R} :

Continuous (star f) ↔ Continuous f

@[simp]

theorem continuous_fun_star_iff {α : Type u_1} {R : Type u_2} [TopologicalSpace R] [InvolutiveStar R] [ContinuousStar R] [TopologicalSpace α] {f : α → R} :

(Continuous fun (i : α) => star (f i)) ↔ Continuous f

Eta-expanded form of continuous_star_iff

@[simp]

theorem continuousAt_star_iff {α : Type u_1} {R : Type u_2} [TopologicalSpace R] [InvolutiveStar R] [ContinuousStar R] [TopologicalSpace α] {f : α → R} {x : α} :

ContinuousAt (star f) x ↔ ContinuousAt f x

@[simp]

theorem continuousAt_fun_star_iff {α : Type u_1} {R : Type u_2} [TopologicalSpace R] [InvolutiveStar R] [ContinuousStar R] [TopologicalSpace α] {f : α → R} {x : α} :

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

Eta-expanded form of continuousAt_star_iff

@[simp]

theorem continuousOn_star_iff {α : Type u_1} {R : Type u_2} [TopologicalSpace R] [InvolutiveStar R] [ContinuousStar R] [TopologicalSpace α] {f : α → R} {s : Set α} :

ContinuousOn (star f) s ↔ ContinuousOn f s

@[simp]

theorem continuousOn_fun_star_iff {α : Type u_1} {R : Type u_2} [TopologicalSpace R] [InvolutiveStar R] [ContinuousStar R] [TopologicalSpace α] {f : α → R} {s : Set α} :

ContinuousOn (fun (i : α) => star (f i)) s ↔ ContinuousOn f s

Eta-expanded form of continuousOn_star_iff

@[simp]

theorem continuousWithinAt_star_iff {α : Type u_1} {R : Type u_2} [TopologicalSpace R] [InvolutiveStar R] [ContinuousStar R] [TopologicalSpace α] {f : α → R} {s : Set α} {x : α} :

ContinuousWithinAt (star f) s x ↔ ContinuousWithinAt f s x

@[simp]

theorem continuousWithinAt_fun_star_iff {α : Type u_1} {R : Type u_2} [TopologicalSpace R] [InvolutiveStar R] [ContinuousStar R] [TopologicalSpace α] {f : α → R} {s : Set α} {x : α} :

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

Eta-expanded form of continuousWithinAt_star_iff

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)

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)

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

ContinuousStar Rᵐᵒᵖ

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

ContinuousStar Rˣ