mathlib3 documentation

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.

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
@[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)