chore(CompHausLike): add constant morphisms (#17381)

leanprover-community · Oct 4, 2024 · 44f94cd · 44f94cd
1 parent 10237af
commit 44f94cd
Showing 1 changed file with 9 additions and 0 deletions.
diff --git a/Mathlib/Topology/Category/CompHausLike/Basic.lean b/Mathlib/Topology/Category/CompHausLike/Basic.lean
@@ -255,4 +255,13 @@ def isoEquivHomeo {X Y : CompHausLike.{u} P} : (X ≅ Y) ≃ (X ≃ₜ Y) where
   left_inv _ := rfl
   right_inv _ := rfl
 
+/-- A constant map as a morphism in `CompHausLike` -/
+def const {P : TopCat.{u} → Prop}
+    (T : CompHausLike.{u} P) {S : CompHausLike.{u} P} (s : S) : T ⟶ S :=
+  ContinuousMap.const _ s
+
+lemma const_comp {P : TopCat.{u} → Prop} {S T U : CompHausLike.{u} P}
+    (s : S) (g : S ⟶ U) : T.const s ≫ g = T.const (g s) :=
+  rfl
+
 end CompHausLike