We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent 59cfdc5 commit 8d8a73dCopy full SHA for 8d8a73d
Mathlib/Topology/Category/Lifting/Separation.lean
@@ -55,9 +55,7 @@ Foobars, barfoos
55
-/
56
57
universe w v u
58
-open CategoryTheory
59
-open TopCat
60
-open Limits Topology TopologicalSpace Set
+open CategoryTheory TopCat Limits Topology TopologicalSpace Set HasLiftingProperty
61
62
@[simp]
63
lemma Concrete.HasPushout.range_inl_union_range_inr
0 commit comments