Zulip Chat Archive
Stream: general
Topic: option.retract
Johan Commelin (Apr 23 2019 at 12:31):
Is this already somewhere in mathlib?
def option.retract {X : Type*} (S : set X) : option X → option S := sorry
Kenny Lau (Apr 23 2019 at 12:35):
more generally an injective function f:A->B induces option B -> option A
Johan Commelin (Apr 23 2019 at 12:49):
Certainly... maybe I should use embeddings
Last updated: May 02 2025 at 03:31 UTC