Replace original namespace with open in pseudoelts

leanprover-community · May 30, 2023 · 48471f3 · 48471f3
1 parent ffaa865
commit 48471f3
Showing 1 changed file with 1 addition and 3 deletions.
diff --git a/counterexamples/pseudoelement.lean b/counterexamples/pseudoelement.lean
@@ -35,7 +35,7 @@ namespace counterexample
 
 noncomputable theory
 
-namespace category_theory.abelian.pseudoelement
+open category_theory.abelian.pseudoelement
 
 /-- `x` is given by `t ↦ (t, 2 * t)`. -/
 def x : over ((of ℤ ℚ) ⊞ (of ℤ ℚ)) :=
@@ -121,6 +121,4 @@ lemma exist_ne_and_fst_eq_fst_and_snd_eq_snd : ∃ x y : (of ℤ ℚ) ⊞ (of
   (biprod.snd : (of ℤ ℚ) ⊞ (of ℤ ℚ) ⟶ _) x = (biprod.snd : (of ℤ ℚ) ⊞ (of ℤ ℚ) ⟶ _) y:=
 ⟨⟦x⟧, ⟦y⟧, mk_x_ne_mk_y, fst_mk_x_eq_fst_mk_y, snd_mk_x_eq_snd_mk_y⟩
 
-end category_theory.abelian.pseudoelement
-
 end counterexample