Skip to content

Commit

Permalink
fix(data/equiv/set): Fix doc comment syntax (#11409)
Browse files Browse the repository at this point in the history
  • Loading branch information
nomeata committed Jan 13, 2022
1 parent 1f370bb commit dfad4c6
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion src/data/equiv/set.lean
Expand Up @@ -478,7 +478,7 @@ by { ext x, simp [(equiv.set.congr f).symm.exists_congr_left] }
end equiv

/-- If a function is a bijection between two sets `s` and `t`, then it induces an
equivalence between the types `↥s` and ``↥t`. -/
equivalence between the types `↥s` and `↥t`. -/
noncomputable def set.bij_on.equiv {α : Type*} {β : Type*} {s : set α} {t : set β} (f : α → β)
(h : set.bij_on f s t) : s ≃ t :=
equiv.of_bijective _ h.bijective
Expand Down

0 comments on commit dfad4c6

Please sign in to comment.