We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent f9cd6b5 commit 11293ffCopy full SHA for 11293ff
1 file changed
Mathlib/Data/Set/Image.lean
@@ -351,7 +351,7 @@ theorem image_eq_preimage_of_inverse {f : α → β} {g : β → α} (h₁ : Lef
351
funext fun s =>
352
Subset.antisymm (image_subset_preimage_of_inverse h₁ s) (preimage_subset_image_of_inverse h₂ s)
353
354
-theorem Involutive.image_eq_preimage {f : α → α} (hf : f.Involutive) :
+theorem _root_.Function.Involutive.image_eq_preimage {f : α → α} (hf : f.Involutive) :
355
image f = preimage f :=
356
image_eq_preimage_of_inverse hf.leftInverse hf.rightInverse
357
0 commit comments