chore(filter/pointwise): protect filter.has_involutive_inv (#14398)

leanprover-community · May 27, 2022 · 25f75c4 · 25f75c4
1 parent 2a9b0f8
commit 25f75c4
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/order/filter/pointwise.lean b/src/order/filter/pointwise.lean
@@ -124,7 +124,7 @@ variables [has_involutive_inv α] {f : filter α} {s : set α}
 
 /-- Inversion is involutive on `filter α` if it is on `α`. -/
 @[to_additive "Negation is involutive on `filter α` if it is on `α`."]
-def has_involutive_inv : has_involutive_inv (filter α) :=
+protected def has_involutive_inv : has_involutive_inv (filter α) :=
 { inv_inv := λ f, map_map.trans $ by rw [inv_involutive.comp_self, map_id],
   ..filter.has_inv }