mathlib3documentation

topology.algebra.star

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]
structure has_continuous_star (R : Type u) [has_star R] :
Prop
• continuous_star :

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

Instances of this typeclass
theorem continuous_on_star {R : Type u_3} [has_star R] {s : set R} :
theorem continuous_within_at_star {R : Type u_3} [has_star R] {s : set R} {x : R} :
theorem continuous_at_star {R : Type u_3} [has_star R] {x : R} :
theorem tendsto_star {R : Type u_3} [has_star R] (a : R) :
theorem filter.tendsto.star {α : Type u_2} {R : Type u_3} [has_star R] {f : α R} {l : filter α} {y : R} (h : (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} [has_star R] {f : α R} (hf : continuous f) :
continuous (λ (x : α), has_star.star (f x))
theorem continuous_at.star {α : Type u_2} {R : Type u_3} [has_star R] {f : α R} {x : α} (hf : x) :
continuous_at (λ (x : α), has_star.star (f x)) x
theorem continuous_on.star {α : Type u_2} {R : Type u_3} [has_star R] {f : α R} {s : set α} (hf : s) :
continuous_on (λ (x : α), has_star.star (f x)) s
theorem continuous_within_at.star {α : Type u_2} {R : Type u_3} [has_star R] {f : α R} {s : set α} {x : α} (hf : x) :
continuous_within_at (λ (x : α), has_star.star (f x)) s x
def star_continuous_map {R : Type u_3} [has_star R]  :
C(R, R)

The star operation bundled as a continuous map.

Equations
@[simp]
theorem star_continuous_map_apply {R : Type u_3} [has_star R] (ᾰ : R) :
@[protected, instance]
def prod.has_continuous_star {R : Type u_3} {S : Type u_4} [has_star R] [has_star 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]
@[protected, instance]
def units.has_continuous_star {R : Type u_3} [monoid R]  :