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
staroperator is continuous.
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}
:
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 := ⋯ }
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
- ⋯ = ⋯