[Merged by Bors] - feat: port Topology.Algebra.Star

Mathlib.lean

@@ -977,6 +977,7 @@ import Mathlib.Topology.Algebra.ConstMulAction
 import Mathlib.Topology.Algebra.Constructions
 import Mathlib.Topology.Algebra.Order.Archimedean
 import Mathlib.Topology.Algebra.Order.LeftRight
+import Mathlib.Topology.Algebra.Star
 import Mathlib.Topology.Bases
 import Mathlib.Topology.Basic
 import Mathlib.Topology.Bornology.Basic

Mathlib/Topology/Algebra/Star.lean

@@ -0,0 +1,103 @@
+/-
+Copyright (c) 2022 Eric Wieser. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Eric Wieser
+
+! This file was ported from Lean 3 source module topology.algebra.star
+! leanprover-community/mathlib commit 4c19a16e4b705bf135cf9a80ac18fcc99c438514
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+import Mathlib.Algebra.Star.Pi
+import Mathlib.Algebra.Star.Prod
+import Mathlib.Topology.Algebra.Constructions
+import Mathlib.Topology.ContinuousFunction.Basic
+
+/-!
+# Continuity of `star`
+
+This file defines the `ContinuousStar` typeclass, along with instances on `Pi`, `Prod`,
+`MulOpposite`, and `Units`.
+-/
+
+open Filter Topology
+
+/-- Basic hypothesis to talk about a topological space with a continuous `star` operator. -/
+class ContinuousStar (R : Type _) [TopologicalSpace R] [Star R] : Prop where
+  /-- The `star` operator is continuous. -/
+  continuous_star : Continuous (star : R → R)
+#align has_continuous_star ContinuousStar
+
+export ContinuousStar (continuous_star)
+
+section Continuity
+
+variable [TopologicalSpace R] [Star R] [ContinuousStar R]
+
+theorem continuousOn_star {s : Set R} : ContinuousOn star s :=
+  continuous_star.continuousOn
+#align continuous_on_star continuousOn_star
+
+theorem continuousWithinAt_star {s : Set R} {x : R} : ContinuousWithinAt star s x :=
+  continuous_star.continuousWithinAt
+#align continuous_within_at_star continuousWithinAt_star
+
+theorem continuousAt_star {x : R} : ContinuousAt star x :=
+  continuous_star.continuousAt
+#align continuous_at_star continuousAt_star
+
+theorem tendsto_star (a : R) : Tendsto star (𝓝 a) (𝓝 (star a)) :=
+  continuousAt_star
+#align tendsto_star tendsto_star
+
+theorem Filter.Tendsto.star {f : α → R} {l : Filter α} {y : R} (h : Tendsto f l (𝓝 y)) :
+    Tendsto (fun x => star (f x)) l (𝓝 (star y)) :=
+  (continuous_star.tendsto y).comp h
+#align filter.tendsto.star Filter.Tendsto.star
+
+variable [TopologicalSpace α] {f : α → R} {s : Set α} {x : α}
+
+-- @[continuity] Porting note: restore attribute
+theorem Continuous.star (hf : Continuous f) : Continuous fun x => star (f x) :=
+  continuous_star.comp hf
+#align continuous.star Continuous.star
+
+theorem ContinuousAt.star (hf : ContinuousAt f x) : ContinuousAt (fun x => star (f x)) x :=
+  continuousAt_star.comp hf
+#align continuous_at.star ContinuousAt.star
+
+theorem ContinuousOn.star (hf : ContinuousOn f s) : ContinuousOn (fun x => star (f x)) s :=
+  continuous_star.comp_continuousOn hf
+#align continuous_on.star ContinuousOn.star
+
+theorem ContinuousWithinAt.star (hf : ContinuousWithinAt f s x) :
+    ContinuousWithinAt (fun x => star (f x)) s x :=
+  Filter.Tendsto.star hf
+#align continuous_within_at.star ContinuousWithinAt.star
+
+/-- The star operation bundled as a continuous map. -/
+@[simps]
+def starContinuousMap : C(R, R) :=
+  ⟨star, continuous_star⟩
+#align star_continuous_map starContinuousMap
+
+end Continuity
+
+section Instances
+
+instance [Star R] [Star S] [TopologicalSpace R] [TopologicalSpace S] [ContinuousStar R]
+    [ContinuousStar S] : ContinuousStar (R × S) :=
+  ⟨(continuous_star.comp continuous_fst).prod_mk (continuous_star.comp continuous_snd)⟩
+
+instance {C : ι → Type _} [∀ i, TopologicalSpace (C i)] [∀ i, Star (C i)]
+    [∀ i, ContinuousStar (C i)] : ContinuousStar (∀ i, C i)
+    where continuous_star := continuous_pi fun i => Continuous.star (continuous_apply i)
+
+instance [Star R] [TopologicalSpace R] [ContinuousStar R] : ContinuousStar Rᵐᵒᵖ :=
+  ⟨MulOpposite.continuous_op.comp <| MulOpposite.continuous_unop.star⟩
+
+instance [Monoid R] [StarSemigroup R] [TopologicalSpace R] [ContinuousStar R] :
+    ContinuousStar Rˣ :=
+  ⟨continuous_induced_rng.2 Units.continuous_embedProduct.star⟩
+
+end Instances