Continuity of star #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This file defines the has_continuous_star typeclass, along with instances on pi, prod,
mul_opposite, and units.
@[class]
- continuous_star : continuous has_star.star
Basic hypothesis to talk about a topological space with a continuous star operator.
theorem
continuous_on_star
{R : Type u_3}
[topological_space R]
[has_star R]
[has_continuous_star R]
{s : set R} :
theorem
continuous_within_at_star
{R : Type u_3}
[topological_space R]
[has_star R]
[has_continuous_star R]
{s : set R}
{x : R} :
theorem
continuous_at_star
{R : Type u_3}
[topological_space R]
[has_star R]
[has_continuous_star R]
{x : R} :
theorem
tendsto_star
{R : Type u_3}
[topological_space R]
[has_star R]
[has_continuous_star R]
(a : R) :
filter.tendsto has_star.star (nhds a) (nhds (has_star.star a))
theorem
filter.tendsto.star
{α : Type u_2}
{R : Type u_3}
[topological_space R]
[has_star R]
[has_continuous_star R]
{f : α → R}
{l : filter α}
{y : R}
(h : filter.tendsto f l (nhds y)) :
filter.tendsto (λ (x : α), has_star.star (f x)) l (nhds (has_star.star y))
@[continuity]
theorem
continuous.star
{α : Type u_2}
{R : Type u_3}
[topological_space R]
[has_star R]
[has_continuous_star R]
[topological_space α]
{f : α → R}
(hf : continuous f) :
continuous (λ (x : α), has_star.star (f x))
theorem
continuous_at.star
{α : Type u_2}
{R : Type u_3}
[topological_space R]
[has_star R]
[has_continuous_star R]
[topological_space α]
{f : α → R}
{x : α}
(hf : continuous_at f x) :
continuous_at (λ (x : α), has_star.star (f x)) x
theorem
continuous_on.star
{α : Type u_2}
{R : Type u_3}
[topological_space R]
[has_star R]
[has_continuous_star R]
[topological_space α]
{f : α → R}
{s : set α}
(hf : continuous_on f s) :
continuous_on (λ (x : α), has_star.star (f x)) s
theorem
continuous_within_at.star
{α : Type u_2}
{R : Type u_3}
[topological_space R]
[has_star R]
[has_continuous_star R]
[topological_space α]
{f : α → R}
{s : set α}
{x : α}
(hf : continuous_within_at f s x) :
continuous_within_at (λ (x : α), has_star.star (f x)) s x
The star operation bundled as a continuous map.
Equations
- star_continuous_map = {to_fun := has_star.star _inst_2, continuous_to_fun := _}
@[simp]
theorem
star_continuous_map_apply
{R : Type u_3}
[topological_space R]
[has_star R]
[has_continuous_star R]
(ᾰ : R) :
@[protected, instance]
def
prod.has_continuous_star
{R : Type u_3}
{S : Type u_4}
[has_star R]
[has_star S]
[topological_space R]
[topological_space S]
[has_continuous_star R]
[has_continuous_star S] :
has_continuous_star (R × S)
@[protected, instance]
def
pi.has_continuous_star
{ι : Type u_1}
{C : ι → Type u_2}
[Π (i : ι), topological_space (C i)]
[Π (i : ι), has_star (C i)]
[∀ (i : ι), has_continuous_star (C i)] :
has_continuous_star (Π (i : ι), C i)
@[protected, instance]
def
mul_opposite.has_continuous_star
{R : Type u_3}
[has_star R]
[topological_space R]
[has_continuous_star R] :
@[protected, instance]
def
units.has_continuous_star
{R : Type u_3}
[monoid R]
[star_semigroup R]
[topological_space R]
[has_continuous_star R] :