Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

Commit 25f75c4

Browse files
committed
chore(filter/pointwise): protect filter.has_involutive_inv (#14398)
1 parent 2a9b0f8 commit 25f75c4

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

src/order/filter/pointwise.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -124,7 +124,7 @@ variables [has_involutive_inv α] {f : filter α} {s : set α}
124124

125125
/-- Inversion is involutive on `filter α` if it is on `α`. -/
126126
@[to_additive "Negation is involutive on `filter α` if it is on `α`."]
127-
def has_involutive_inv : has_involutive_inv (filter α) :=
127+
protected def has_involutive_inv : has_involutive_inv (filter α) :=
128128
{ inv_inv := λ f, map_map.trans $ by rw [inv_involutive.comp_self, map_id],
129129
..filter.has_inv }
130130

0 commit comments

Comments
 (0)