From abd65d5041585a6b8db39dde8c2ac4414b584b06 Mon Sep 17 00:00:00 2001 From: Matthew Robert Ballard Date: Wed, 5 Jul 2023 06:02:46 +0000 Subject: [PATCH] =?UTF-8?q?chore:=20rescope=20=CE=A9=20notation=20for=20Lo?= =?UTF-8?q?opSpace=20(#5714)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Mathlib/Topology/Homotopy/HomotopyGroup.lean | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/Mathlib/Topology/Homotopy/HomotopyGroup.lean b/Mathlib/Topology/Homotopy/HomotopyGroup.lean index 13a75cfc3916a..968ff901d52d8 100644 --- a/Mathlib/Topology/Homotopy/HomotopyGroup.lean +++ b/Mathlib/Topology/Homotopy/HomotopyGroup.lean @@ -94,7 +94,7 @@ def LoopSpace := #align loop_space LoopSpace -- mathport name: exprΩ -scoped[Topology] notation "Ω" => LoopSpace +scoped[Topology.Homotopy] notation "Ω" => LoopSpace instance LoopSpace.inhabited : Inhabited (Path x x) := ⟨Path.refl x⟩ @@ -107,7 +107,9 @@ def GenLoop : Set C(I^N, X) := {p | ∀ y ∈ Cube.boundary N, p y = x} #align gen_loop GenLoop -scoped[Topology] notation "Ω^" => GenLoop +scoped[Topology.Homotopy] notation "Ω^" => GenLoop + +open Topology.Homotopy variable {N X x}