mathlib3 documentation

core / init.data.option.instances

@[protected, instance]
theorem option.eq_of_eq_some {α : Type u} {x y : option α} :
( (z : α), x = option.some z y = option.some z) x = y
theorem option.eq_some_of_is_some {α : Type u} {o : option α} (h : (o.is_some)) :
theorem option.eq_none_of_is_none {α : Type u} {o : option α} :