feat(Data/Opposite): Show that op, unop are surjective (#11240)

leanprover-community · Mar 26, 2024 · d4c2327 · d4c2327
1 parent 6d8ec38
commit d4c2327
Showing 1 changed file with 4 additions and 0 deletions.
diff --git a/Mathlib/Data/Opposite.lean b/Mathlib/Data/Opposite.lean
@@ -89,6 +89,10 @@ def equivToOpposite : α ≃ αᵒᵖ where
   right_inv := op_unop
 #align opposite.equiv_to_opposite Opposite.equivToOpposite
 
+theorem op_surjective : Function.Surjective (op : α → αᵒᵖ) := equivToOpposite.surjective
+
+theorem unop_surjective : Function.Surjective (unop : αᵒᵖ → α) := equivToOpposite.symm.surjective
+
 @[simp]
 theorem equivToOpposite_coe : (equivToOpposite : α → αᵒᵖ) = op :=
   rfl